|
@@ -199,7 +199,66 @@ We also introduce a new subsumption typing rule:
|
|
|
\inference{\Gamma \vdash e : S & S <: T}{\Gamma \vdash e : T}
|
|
|
\]
|
|
|
|
|
|
-% TODO : booléens… (autre photo)
|
|
|
+Assignment
|
|
|
+\[
|
|
|
+ \inference{\Gamma \vdash x : T & \Gamma \vdash a : T}{\Gamma \vdash x := a}
|
|
|
+\]
|
|
|
+
|
|
|
+Sequence
|
|
|
+\[
|
|
|
+ \inference{\Gamma \vdash S_1 & \Gamma \vdash S_2}{\Gamma \vdash (S_1 ; S_2)}
|
|
|
+\]
|
|
|
+
|
|
|
+While loop
|
|
|
+\[
|
|
|
+ \inference{\Gamma \vdash b & \Gamma \vdash S}{\Gamma \vdash \<while>\ b\ \<do>\ S}
|
|
|
+\]
|
|
|
+
|
|
|
+Condition
|
|
|
+\[
|
|
|
+ \inference{\Gamma \vdash b & \Gamma \vdash S_1 & \Gamma \vdash S_2}{\Gamma \vdash \<if>\ b\ \<then>\ S_1\ \<else>\ S_2}
|
|
|
+\]
|
|
|
+
|
|
|
+Booleans
|
|
|
+\[
|
|
|
+ \inference{}{\Gamma \vdash \<true>}
|
|
|
+\]
|
|
|
+\[
|
|
|
+ \inference{}{\Gamma \vdash \<false>}
|
|
|
+\]
|
|
|
+\[
|
|
|
+ \inference{\Gamma \vdash b}{\Gamma \vdash \<not>\ b}
|
|
|
+\]
|
|
|
+\[
|
|
|
+ \inference{\Gamma \vdash b_1 & \Gamma \vdash b_2}{\Gamma \vdash b_1\ o\ b_2}{o \in \{\<and>, \<or>\}}
|
|
|
+\]
|
|
|
+\[
|
|
|
+ \inference{\Gamma \vdash a_1 : int & \Gamma \vdash a_2 : int}{\Gamma \vdash a_1 \le a_2}
|
|
|
+\]
|
|
|
+\[
|
|
|
+ \inference{\Gamma \vdash a_1 : T & \Gamma \vdash a_2 : T}{\Gamma \vdash a_1 = a_2}
|
|
|
+\]
|
|
|
+Note: for the equality test, the rule works for \<int> as well as for records.
|
|
|
+
|
|
|
+% Domains
|
|
|
+\[
|
|
|
+ n \in Num
|
|
|
+\]
|
|
|
+\[
|
|
|
+ x \in Var
|
|
|
+\]
|
|
|
+\[
|
|
|
+ e,e_1,e_2,a,a_1,a_2 \in AExpr
|
|
|
+\]
|
|
|
+\[
|
|
|
+ b,b_1,b_2 \in BExpr
|
|
|
+\]
|
|
|
+\[
|
|
|
+ f,f_1,\dots,f_n,f_i,g_1,\dots,g_k, \in Field % Field n'est pas défini…
|
|
|
+\]
|
|
|
+\[
|
|
|
+ S,S_1,S_2 \in Statement
|
|
|
+\]
|
|
|
|
|
|
\subsection{Correctness}
|
|
|
|