semantique_avec_routine
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.
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.
Inductive prog : Set :=
NOPE: prog
| AFF: nat ⟶ exp ⟶ prog
| SEQ: prog ⟶ prog ⟶ prog
| IFTE: exp ⟶ prog ⟶ prog ⟶ prog
| WHILE: exp ⟶ prog ⟶ prog
| CALL: nat ⟶ 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()'" := (CALL 1) : Prog_scope.
Notation "'g()'" := (CALL 2) : Prog_scope.
Notation "'h()'" := (CALL 3) : Prog_scope.
Module Ex_prog.
Exemples de programme;
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) des
états (ou environnements) vers les états.
Inductive eval_prog (π:gen_env 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 σ' pbody,
Ext.binds prc pbody π ⟶
《 σ, pbody, π 》 ⟿ σ' ⟶
_____________
《 σ, CALL prc, π 》 ⟿ σ'
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