semantique
Ce module formalise la sémantique d'un petit langage impératif. Il
n'y a pas de fonction ni de procédure.
La sémantique d'un langage décrit formellement le comportement des
expressions et des instructions de ce langage. C'est la
"définition" du langage. Pour les expressions il s'agit de définir
quelle est la valeur calculée par une expression. Pour une
instruction il s'agit de décrire les effets des instructions sur
les variables du programme (plus généralement les effets d'un
programme peuvent aussi inclure les entrées/sorties mais nous ne
considérons pas cela ici).
La sémantique des expression est composée de jugements de la forme
《 σ, e 》↦ v, où σ est l'enironnement d'exécution qui contient
les valeurs des variables du programme, p est l'expression à
évaluer et v sa valeur.
La sémantique des instructions sera composée de jugements de la
forme 《 σ, NOPE 》 ⟿ σ', où σ est l'enironnement d'exécution
avant l'exécution du programme p et σ' est l'environnement après
l'exécution de p (les variables ont changé de valeur). On exprime
en général cette sémantique sous la forme de règles d'inférence,
ce qui s'écrit en Coq par une relation inductive où chaque
constructeur correspond à une règle.
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
.
On utilisera les notations suivante pour désigner les expressions
de manière plus lisible.
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 est l'union de
l'ensemble des entiers et des booléen. On utlise un type inductif
à deux constructeurs.
La relation d'interprétation des expressions. Aussi appelée la
sémantique des expressions. Afin de présenter la sémantique sous
la forme de règles d'inférences, on utilise des barres
horizontales. Ces barres n'ont pas de signification (elles sont
ignorées par Coq) autre que celle de rappeler la forme des règles
d'inférence. Autrement dit la propriété suivante:
Ext.binds i v σ ⟶
_____________
《 σ, VAR i 》↦ v
est équivalente à Ext.binds i v σ ⟶ 《 σ, VAR i 》↦ v.
Notez que pour des raisons de simplicité on ne définit pas la
sémantique de la division. En effet cela nécessiterait de traiter le
cas de la division par zéro.
Ext.binds i v σ ⟶
_____________
《 σ, VAR i 》↦ v
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.
| 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.
Exemple de jugement prouvable.
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.
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.
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 : 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 》 ⟿ σ'
where " '《' A ',' B '》' '⟿' C " := (eval_prog B A C) : Prog_scope.
Lemma determinisme_prog :
forall σ p σ', 《σ,p》 ⟿ σ' ⟶ forall σ'', 《σ,p》 ⟿ σ'' ⟶ σ' ≡ σ''.
This page has been generated by coqdoc