Table of Contents

LANGAGES ET TRADUCTEURS – Chapitre 6 Jean-François Monin, 2021

1 Le langage While

1.1 Syntaxe

Inductive aexp : Set :=
  | Cst : nat -> aexp
  | Ava : nat -> aexp
  | Apl : aexp -> aexp -> aexp
  | Amu : aexp -> aexp -> aexp
.

Inductive bexp :=
| Btrue : bexp
| Bfalse : bexp
| Bnot : bexp -> bexp
| Band : bexp -> bexp -> bexp
| Bor : bexp -> bexp -> bexp
| Beqnat : aexp -> aexp -> bexp (* test égalité d'aexp *)
.

Inductive winstr :=
| Skip   : winstr
| Assign : nat -> aexp -> winstr
| Seq    : winstr -> winstr -> winstr
| If     : bexp -> winstr -> winstr -> winstr
| While  : bexp -> winstr -> winstr
.

1.2 Remarque sur les expressions aexp et bexp

La distinction entre expressions arithmétiques et expressions booléennes est rendue ici sous une forme particulièrement stricte. On pourrait facilement imaginer un opérateur de comparaison entre des expressions booléennes, qui au niveau textuel serait aussi rendu par un symbole tel que "=" (à la C) ou "" (à la Algol).

L'approche qui passe à l'échelle des langages usuels consiste à n'avoir qu'un seul type pour tous les AST d'expressions. On est alors conduit à considérer des AST pour des expressions telles que false + true ou 3 && 5, pour lesquels on ne désire pas donner de sémantique (la fonction eval peut donner soit un résultat factice, soit "ne pas" donner de résultat). Ou alors à donner une sémantique sous réserve que l'espression soit "bien typée" : cela passe par la formalisation d'une notion de typage pour nos AST d'expressions.

Le compromis qui est fait ici, issu de [Nielson&Nielson] revient à graver dans la syntaxe une information de typage. C'est inhabituel mais permet d'avoir un peu d'organisation à bas coût pour se focaliser rapidement sur les notions de sémantique dynamique. En fonction du temps disponible, on verra plus tard comment traiter des expressions plus générales.

1.3 Comment exprimer la sémantique du langage While

Que dit un programme sous forme d'AST winstr ?

1.3.1 Réponse

Il a un effet sur une mémoire (de type state)

Comment énoncer cet effet ?

1.3.2 Idée 1

Fonction changeetat : state -> winstr -> state

Mais on verra que ça ne marche pas complètement

1.3.3 Idée 2

Relation changeetat : state -> winstr -> state -> Prop

On a besoin de la généralité de Prop (bool est inadapté, cf avant-goût sur eqnatb).

Par exemple on voudra prouver que si P1 est un (AST de) programme, et que P2 est l'AST obtenu à partir de PA en effectuant certaines optimisations, alors pour tout état initial, l'état final obtenu après l'exécution de P2 est le même que celui obtenu après l'éxécution de P1.

1.3.4 Besoin

  • Exprimer des relations de façon générale.
  • Technique centrale : relations inductives.
  • Exemples vus en PF : relation d'évaluation et de typage (avec un environnement au lieu d'un état).

2 Sémantique relationnelle "naturelle" (SN) du langage WHILE

Prérequis : relations inductives (chap 06)

2.1 Langage

Inductive winstr :=
| Skip   : winstr
| Assign : nat -> aexp -> winstr
| Seq    : winstr -> winstr -> winstr
| If     : bexp -> winstr -> winstr -> winstr
| While  : bexp -> winstr -> winstr
.

2.1.1 Choix conceptuels

  1. pourquoi Assign 3 (Ava 5) et non Assign (Ava 3) (Ava 5)
  2. ouverture sur l'adressage à la C

2.2 Tentative de sémantique fonctionnelle

Fixpoint update (i:nat) (v:nat) (s:state) : state :=
  match i, s with
  | 0,    _ :: s'   => v  :: s'
  | 0,    []        => v  :: []
  | S i', v' :: s'  => v' :: update i' v s'
  | S i', []        => 0  :: update i' v []
  end.

Fixpoint evalW (i : winstr) (s : state) {struct i} : state :=
  match i with
  | Skip       => s
  | Assign x e => update x (evalA e s) s
  | Seq i1 i2  => let s1 := evalW i1 s in evalW i2 s1
               (*   (evalW i2 (evalW i1 s) *)
  | If e i1 i2 => match evalB e s with
                  | true  => evalW i1 s
                  | false => evalW i2 s
                  end
  | (While e i1) as i => match evalB e s with
                  | true  =>
                    let s1 := evalW i1 s in evalW (While e i1) s1
               (*   let s1 := evalW i1 s in evalW i s1                *)
                  | false => s
                  end
  end.

NB : {struct i} annonce que la décroissance structurelle est attendue sur i (indication pouvant être omise très souvent).

2.2.1 Problème : evalW (While e i1) s1 ne respecte pas cette contrainte

Attention : le fait d'avoir s1 à la place de s ne garantit RIEN

  • s1 peut être identique à s exemple : While Btrue Skip
  • ou pas While (Bnot (Beqnat (Ava 1) (Aco 0))) (Assign 1 (Apl (Ava 1) (Aco 1))) (* ! x1 = 0 ) ( x1 := x1 + 1 *)
  • ou chaotique fonction de Collatz-Syracuse

2.2.2 Par contre on peut l'écrire en OCaml

Problème :

  1. qu'est-ce que cela signifie ?
  2. quelle est la sémantique de OCaml ?

2.2.3 fonctions partielles

Raisonner directement dessus de façon rigoureuse n'est pas commode On parsème des "conditions à respecter", beaucoup d'opportunités pour les oublis involontaires…

2.3 Des fonctions aux relations

2.3.1 Exemple

  1. Au TD2, coulsuiv : coulfeu -> coulfeu
  2. code
    fun c => match c with
  | vert => orange
  | orange => rouge
  | rouge => vert
  end
  3. Au TD5, coulsuiv : "coul -> coul"

    mais indéfinie pour jaune, bleu etc.

    On définit à la place une relation coulsuiv : coul -> coul -> Prop

  4. code
    Inductive coulsuiv : coul -> coul -> Prop :=
| CSv : coulsuiv vert orange
| CSo : coulsuiv orange rouge
| CSr : coulsuiv rouge vert
.

2.3.2 Idée générale

Au lieu d'une fonction f de type A1 -> A2 ->… -> B prendre une relation R de type A1 -> A2 ->… -> B -> Prop telle que l'on ait toujours R a1 a2 … (f a1 a2 …)

2.3.3 Remarque : une relation peut aussi être non-déterministe

A partir des mêmes entrées on peut aboutir à plusieurs résultats Exemple possible. 

Inductive coulsuiv : coul -> coul -> Prop :=
| CSv  : coulsuiv vert orange
| CSo  : coulsuiv orange rouge
| CSr  : coulsuiv rouge vert
| CSr' : coulsuiv rouge bleu
.

2.4 Application : sémantique relationnelle de While

Dite sémantique naturelle (SN) Ou encore sémantique opérationnelle à grands pas 

Inductive SN: winstr -> state -> state -> Prop :=
| SN_Skip        : forall s,
                   SN Skip s s
| SN_Assign      : forall x e s,
                   SN (Assign x e) s (update x (evalA e s) s)
| SN_Seq         : forall i1 i2 s s1 s2,
                   SN i1 s s1 -> SN i2 s1 s2 -> SN (Seq i1 i2) s s2
| SN_If_true     : forall e i1 i2 s s1,
                   (evalB e s = true)  ->  SN i1 s s1 -> SN (If e i1 i2) s s1
| SN_If_false    : forall e i1 i2 s s2,
                   (evalB e s = false) ->  SN i2 s s2 -> SN (If e i1 i2) s s2
| SN_While_false : forall e i s,
                   (evalB e s = false) ->  SN (While e i) s s
| SN_While_true  : forall e i s s1 s2,
                   (evalB e s = true)  ->  SN i s s1 -> SN (While e i) s1 s2
               ->  SN (While e i) s s2
.

2.4.1 Représentation traditionnelle par des règles (cf. PF)


evalB e s = true   SN i s s1    SN (While e i) s1 s2
----------------------------------------------------  SN_While_true
                SN (While e i) s s2



                       i              While e i
evalB e s = true    s ---> s1    s1 ------------> s2

----------------------------------------------------  SN_While_true

                      While e i
                s ---------------> s2

Le fait que, à partir d'un état initial s0, l'exécution d'un programme P aboutit à l'état final sf se traduit par l'existence d'une preuve de SN P s0 sf, autrement dit, l'existence d'un arbre de preuve de conclusion 


        P
s0 ----------> sf

On sera amené à raisonner sur de tels arbres de preuve

D'où les entraînements sur even, p2p7, mul4, coulsuivestCoulfeu.

3 Propriétés issues de la SN

Author: jf

Created: 2021-10-19 mar. 17:24

Validate