semantique_avec_procedure
Ce module formalise la sémantique d'un petit langage impératif.
Reserved Notation "x ;; y" (at level 70, right associativity).
Inductive exp : Set :=
| TRUE: exp
| FALSE: exp
| CST: nat ⟶ exp
| VAR: nat ⟶ exp
| PLUS: exp ⟶ exp ⟶ exp
| MINUS: exp ⟶ exp ⟶ exp
| OPP: exp ⟶ exp ⟶ exp
| MULT: exp ⟶ exp ⟶ exp
| DIV: exp ⟶ exp ⟶ exp
| AND: exp ⟶ exp ⟶ exp
| OR: exp ⟶ exp ⟶ exp
| NOT: exp ⟶ exp.
Notation "A + B" := (PLUS A B) : Prog_scope.
Notation "A - B" := (MINUS A B) : Prog_scope.
Notation "A * B" := (MULT A B) : Prog_scope.
Notation "A / B" := (DIV A B) : Prog_scope.
Notation "A && B" := (AND A B) : Prog_scope.
Notation "A || B" := (OR A B) : Prog_scope.
Notation "! A" := (NOT A) (at level 45) : Prog_scope.
Notation "´X´" := (VAR 1): Prog_scope.
Notation "´Y´" := (VAR 2): Prog_scope.
Notation "´Z´" := (VAR 3): Prog_scope.
Notation "´T´" := (VAR 4): Prog_scope.
Le domaine d'interprétation des expressions
La sémantique opérationnelle à grands pas des expressions
Notation "´__________________´ P2" := (P2) (at level 90, P2 at level 200, right associativity, only parsing).
Notation "´____________________________________´ P2" := (P2) (at level 90, P2 at level 200, right associativity, only parsing).
La relation d'interprétation des expressions. Aussi appelée la
sémantique des expressions.
Inductive eval_exp (σ:gen_env value): exp ⟶ value ⟶ Prop :=
| Eval_Var: forall i v,
Ext.binds i v σ ⟶
_____________
《 σ, VAR i 》↦ v
| Eval_TRUE:
_____________
《 σ, TRUE 》 ↦ Bool true
| Eval_FALSE:
_____________
《 σ, FALSE 》 ↦ Bool false
| Eval_CST: forall i,
_____________
《 σ, CST i 》 ↦ Int i
| Eval_NOT: forall e v v´,
《 σ , e 》 ↦ (Bool v´) ⟶
v = negb v´ ⟶
_____________
《 σ , ! e 》 ↦ Bool v
| Eval_AND: forall e1 v1 e2 v2 v,
《 σ , e1 》 ↦ (Bool v1) ⟶
《 σ , e2 》 ↦ (Bool v2) ⟶
v = andb v1 v2 ⟶
_____________
《 σ , e1 && e2 》 ↦ Bool v
| Eval_OR: forall e1 v1 e2 v2 v,
《 σ , e1 》 ↦ (Bool v1) ⟶
《 σ , e2 》 ↦ (Bool v2) ⟶
v = orb v1 v2 ⟶
_____________
《 σ , e1 || e2 》 ↦ Bool v
| Eval_PLUS: forall e1 v1 e2 v2 v,
《 σ , e1 》 ↦ (Int v1) ⟶
《 σ , e2 》 ↦ (Int v2) ⟶
v = (v1 +v2)%nat ⟶
_____________
《 σ , e1 + e2 》 ↦ Int v
| Eval_MINUS: forall e1 v1 e2 v2 v,
《 σ , e1 》 ↦ (Int v1) ⟶
《 σ , e2 》 ↦ (Int v2) ⟶
v = (v1 - v2)%nat ⟶
_____________
《 σ , e1 - e2 》 ↦ Int v
| Eval_MULT: forall e1 v1 e2 v2 v,
《 σ , e1 》 ↦ (Int v1) ⟶
《 σ , e2 》 ↦ (Int v2) ⟶
v = (v1 × v2)%nat ⟶
_____________
《 σ , e1 × e2 》 ↦ Int v
where " ´《´ A ´,´ B ´》´ ´↦´ C " := (eval_exp A B C) : Prog_scope.
Function eval_exp_list (σ:gen_env value) (le:list exp) (lv:list value) {struct le} : Prop :=
match le with
| nil =>
match lv with
| cons v lv´ => False
| nil => True
end
| cons e le´ =>
match lv with
| cons v lv´ => eval_exp σ e v ∧ eval_exp_list σ le´ lv´
| nil => False
end
end.
Lemma eval_exp1 : 《(ENV.Core.empty _) , CST 1 + CST 2 》 ↦ Int 3.
Print eval_exp1.
Preuve du déterminisme de la sémantique des expressions.
Lemma determinisme_exp :
forall σ e v, 《σ,e》 ↦ v ⟶ forall v´, 《σ,e》 ↦ v´ ⟶ v = v´.
Corollary deterministe_eval_exp_list: forall σ le lv lv´,
eval_exp_list σ le lv
⟶ eval_exp_list σ le lv´
⟶ lv = lv´.
Inductive prog : Set :=
NOPE: prog
| AFF: nat ⟶ exp ⟶ prog
| SEQ: prog ⟶ prog ⟶ prog
| IFTE: exp ⟶ prog ⟶ prog ⟶ prog
| WHILE: exp ⟶ prog ⟶ prog
| CALL: nat ⟶ list exp ⟶ prog.
Quelques notations pour y voir plus clair.
Notation "A ;; B" := (SEQ A B): Prog_scope.
Notation "N ← B" := (AFF N B) (at level 65): Prog_scope.
Notation "´X´ ← B" := (AFF 1 B) (at level 65): Prog_scope.
Notation "´Y´ ← B" := (AFF 2 B) (at level 65): Prog_scope.
Notation "´Z´ ← B" := (AFF 3 B) (at level 65): Prog_scope.
Notation "´T´ ← B" := (AFF 4 B) (at level 65): Prog_scope.
Notation "´IF´ A ´THEN´ B ´ELSE´ C" := (IFTE A B C) (at level 200): Prog_scope.
Notation "´WHILE´ A ´DO´ B ´DONE´" := (WHILE A B) (at level 71): Prog_scope.
Notation "´f(´ L ´)´" := (CALL 1 L) : Prog_scope.
Notation "´g(´ L ´)´" := (CALL 2 L) : Prog_scope.
Notation "´h(´ L ´)´" := (CALL 3 L) : Prog_scope.
Module Ex_prog.
Exemples de programme;
Definition prog1:prog :=
WHILE TRUE DO
NOPE ;;
X ← CST(2) + X;;
Y ← Y + Z;;
f( (X :: (CST(2) + Y)::nil) )
DONE.
End Ex_prog.
La sémantique (opérationnelle, à grands pas) des programmes
La relation d'interprétation des programmes, aussi appelée la
sémantique des programmes. Le domaine d'interprétation est
gen_env value c'est-à-dire qu'un programme est interprété comme
une fonction (partielle, certains programmes ne termine pas ou
n'ont pas de signification) des états (ou environnements) vers les
états.
À la différence des définitions précédentes (sémantiques sans
procédure), on n'utilise plus l'équivalence sur les environnement,
mais l'égalité stricte. Cela permet de simplifier les preuves sur
le pop.
Print Scopes.
Inductive eval_prog (π:gen_env (list nat×prog)) : prog ⟶ gen_env value ⟶ gen_env value ⟶ Prop :=
| Eval_NOPE: forall σ σ´,
σ = σ´ ⟶
_____________
《 σ, NOPE, π 》 ⟿ σ´
| Eval_Seq: forall σ p1 σ´ p2 σ´´,
《 σ, p1, π 》 ⟿ σ´ ⟶
《 σ´, p2, π 》 ⟿ σ´´ ⟶
_____________
《 σ, p1;;p2, π 》 ⟿ σ´´
| Eval_Aff: forall σ e i v σ´,
《 σ, e 》 ↦ v ⟶
σ´ = σ [ i <- v] ⟶
_____________
《 σ, i ← e, π 》 ⟿ σ´
| Eval_If_then: forall σ e p1 p2 σ´,
《 σ, e 》 ↦ Bool true ⟶
《 σ, p1, π 》⟿ σ´ ⟶
_____________
《 σ, (IF e THEN p1 ELSE p2), π 》 ⟿ σ´
| Eval_If_else: forall σ e p1 p2 σ´,
《 σ, e 》 ↦ Bool false ⟶
《 σ, p2, π 》⟿ σ´ ⟶
_____________
《 σ, (IF e THEN p1 ELSE p2), π 》 ⟿ σ´
| Eval_While_true: forall σ e p σ´ σ´´,
《 σ, e 》 ↦ Bool true ⟶
《 σ, p, π 》 ⟿ σ´ ⟶
《 σ´, WHILE e DO p DONE, π 》⟿ σ´´ ⟶
_____________
《 σ, WHILE e DO p DONE, π 》 ⟿ σ´´
| Eval_While_false: forall σ e p σ´,
σ = σ´ ⟶
《 σ, e 》 ↦ Bool false ⟶
_____________
《 σ, WHILE e DO p DONE, π 》 ⟿ σ´
| Eval_Proc: forall σ prc lid le lv σproc σ´ σ´´ pbody,
Ext.binds prc (lid,pbody) π ⟶
eval_exp_list σ le lv ⟶
pushl lid lv σ = Some σproc ⟶
《 σproc , pbody, π 》 ⟿ σ´ ⟶
pop_forgetl (List.length lv) σ´ = Some σ´´ ⟶
_____________
《 σ, CALL prc le, π 》 ⟿ σ´´
where " ´《´ A ´,´ B ´,´ C ´》´ ´⟿´ D " := (eval_prog C B A D) : Prog_scope.
Lemma determinisme_prog :
forall π σ p σ´, 《σ,p,π》 ⟿ σ´ ⟶ forall σ´´, 《σ,p,π》 ⟿ σ´´ ⟶ σ´ = σ´´.
This page has been generated by coqdoc