Creative Commons License Copyright Pierre Courtieu et Olivier Pons. This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International public License.

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.

Les expressions

Le type des expressions entières et booléennes


Inductive exp : Set :=
| TRUE: exp
| FALSE: exp
| CST: natexp
| VAR: natexp
| PLUS: expexpexp
| MINUS: expexpexp
| OPP: expexpexp
| MULT: expexpexp
| DIV: expexpexp
| AND: expexpexp
| OR: expexpexp
| NOT: expexp




.

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.
Inductive value : Set :=
  Bool: boolvalue
| Int: natvalue.

La sémantique opérationnelle à grands pas des expressions



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.
Inductive eval_exp (σ:gen_env value): expvalueProp :=
| 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.

Lemma eval_exp1 : 《(ENV.Core.empty _) , CST 1 + CST 2 Int 3.
Preuve du déterminisme de la sémantique des expressions.

Lemma determinisme_exp :
  forall σ e v, σ,e vforall v', σ,e v'v = v'.

Les programmes

Le type des programmes


Inductive prog : Set :=
  NOPE: prog
| AFF: natexpprog
| SEQ: progprogprog
| IFTE: expprogprogprog
| WHILE: expprogprog.

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;

  Definition prog1:prog :=
    WHILE TRUE DO
      NOPE ;;
      X CST(2) + X;;
      Y Y + Z
    DONE.

End Ex_prog.


La sémantique (opérationnelle, à grands pas) des programmes

On note E F lorsque E et F sont deux environnements (deux états) équivalents (les variables ont les mêmes valeurs).

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 : proggen_env valuegen_env valueProp :=
| 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