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.

loglangcoq.logique.semantique







Sémantique simple

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 expressions 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, e est l'expression à évaluer et v sa valeur.
La sémantique des instructions sera composée de jugements de la forme 《 σ, p 》 ⟿ σ', 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 et les nouvelles valeur (apparaissant dans σ') sont exprimées en fonction des anciennes (celle de σ).
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: 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.
Inductive value : Set :=
  Bool: bool ⟶ value
| Int: nat ⟶ value.

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): 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.


Exemple de jugement prouvable.

Lemma eval_exp1 : 《(ENV.Core.empty _) , CST 1 + CST 2 》 ↦ Int 3.
Proof.
  apply (Eval_PLUS _ _ 1 _ 2).
  apply Eval_CST.
  apply Eval_CST.
  reflexivity.
Qed.
Preuve du déterminisme de la sémantique des expressions.

Lemma determinisme_exp :
  forall σ e v, 《σ,e》 ↦ v ⟶ forall v', 《σ,e》 ↦ v' ⟶ v = v'.
Proof.
  intros σ e x semv.
  induction semv; intros x' semx'.
  - inversion semx';subst.
    eapply Ext.binds_eq_inv;eauto.
  - inversion semx';subst. trivial.
  - inversion semx';subst. trivial.
  - inversion semx';subst. trivial.
  - inversion semx';subst.
    apply IHsemv in H1.
    inversion H1.
    auto.
  - inversion semx';subst.
    apply IHsemv1 in H2.
    apply IHsemv2 in H3.
    inversion H2.
    inversion H3.
    auto.
  - inversion semx';subst.
    apply IHsemv1 in H2.
    apply IHsemv2 in H3.
    inversion H2.
    inversion H3.
    auto.
  - inversion semx';subst.
    apply IHsemv1 in H2.
    apply IHsemv2 in H3.
    inversion H2.
    inversion H3.
    auto.
  - inversion semx';subst.
    apply IHsemv1 in H2.
    apply IHsemv2 in H3.
    inversion H2.
    inversion H3.
    auto.
  - inversion semx';subst.
    apply IHsemv1 in H2.
    apply IHsemv2 in H3.
    inversion H2.
    inversion H3.
    auto.
Qed.

Les programmes

Le type des programmes


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;

  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 : 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》 ⟿ σ'' ⟶ σ' ≡ σ''.
Proof.
  intros σ p σ' Hσ'.
  induction Hσ'; try (rename σ'' into σaux) ; intros σ'' Hσ''.

  - inversion Hσ'';auto.
    transitivity σ;auto.

  - inversion Hσ'';subst;eauto.
    inversion Hσ'';subst.
    assert (σ' ≡ σ'0).
    + apply IHHσ'1;auto.
    + eapply IHHσ'2;eauto.
      rewrite H;auto.

  - inversion Hσ'';subst.
    assert (heq: v = v0 ).
    eapply determinisme_exp;eauto.
    rewrite heq in ×.
    eauto.

  - inversion Hσ'';subst.
    apply IHHσ';auto.
    absurd (Bool false = Bool true).
    intro.
    inversion H0.
    eapply determinisme_exp;eauto.

  - inversion Hσ'';subst.
    absurd (Bool false = Bool true).
    intro.
    inversion H0.
    eapply determinisme_exp;eauto.
    apply IHHσ';auto.

  - inversion Hσ'';subst.
    + assert (σ' ≡ σ'0).
      { apply IHHσ'1;auto. }
      eapply IHHσ'2;eauto.
      rewrite H0;auto.
    + eapply IHHσ'2;eauto.
      absurd (Bool false = Bool true).
      intro.
      inversion H0.
      eapply determinisme_exp;eauto.

  - inversion Hσ'';subst.
    absurd (Bool false = Bool true).
    intro.
    inversion H1.
    eapply determinisme_exp;eauto.
    eauto.
Qed.

This page has been generated by coqdoc