TD du mardi 8 mars

On devra travailler avec les définitions suivantes:

 
Require Export ZArith String.
Require Export List.
Open Scope Z_scope.
Open Scope string_scope.
 
Inductive aexpr : Type :=
  avar (s:string) | anum (x:Z) | aplus (e1 e2 : aexpr).
 
Inductive bexpr : Set :=
  blt (e1 e2 : aexpr).
 
Inductive instr : Type:=
  skip | assign (s:string) (e:aexpr) 
| sequence (i1 i2 : instr) | while (b : bexpr) (i:instr).
 
Definition env := list (string * Z).
 
Inductive aeval : env -> aexpr -> Z -> Prop :=
  ae_num : forall r n, aeval r (anum n) n
| ae_var1 : forall r x v, aeval ((x,v)::r) (avar x) v
| ae_var2 : forall r x y v v' , x <> y -> aeval r (avar x) v' ->
              aeval ((y,v)::r) (avar x) v'
| ae_plus : forall r e1 e2 v1 v2,
              aeval r e1 v1 -> aeval r e2 v2 ->
              aeval r (aplus e1 e2) (v1 + v2).
 
Inductive beval : env -> bexpr -> bool -> Prop :=
| be_lt1 : forall r e1 e2 v1 v2,
            aeval r e1 v1 -> aeval r e2 v2 ->
            v1 < v2 -> beval r (blt e1 e2) true
| be_lt2 : forall r e1 e2 v1 v2,
            aeval r e1 v1 -> aeval r e2 v2 ->
            v2 <= v1 -> beval r (blt e1 e2) false.
 
Inductive update : env->string->Z->env->Prop :=
| s_up1 : forall r x v v', update ((x,v)::r) x v' ((x,v')::r)
| s_up2 : forall r r' x y v v', update r x v' r' ->
            x <> y -> update ((y,v)::r) x v' ((y,v)::r').
 
Inductive exec : env->instr->env->Prop :=
| SN1 : forall r, exec r skip r
| SN2 : forall r r' x e v,
   aeval r e v -> update r x v r' -> exec r (assign x e) r'
| SN3 : forall r r' r'' i1 i2,
    exec r i1 r' -> exec r' i2 r'' ->
    exec r (sequence i1 i2) r''
| SN4 : forall r r' r'' b i,
    beval r b true -> exec r i r' -> 
    exec r' (while b i) r'' ->
    exec r (while b i) r''
| SN5 : forall r b i,
    beval r b false -> exec r (while b i) r.

Raisonner par cas sur une dérivation

Démontrer l'énoncé suivant: pour n'importe quelles trois instruction i1, i2 et i3 et n'importe quels environnements r et r', si exec r (sequence i1 (sequence i2 i3)) r' est prouvable alors exec r (sequence (sequence i1 i2) i3) r' est également prouvable.

Raisonner par récurrence sur une dérivation

On considère les définitions de fonction suivantes

 
Fixpoint lku (s : env) (x : string) : Z :=
  match s with
    nil => 0
  | (y, n)::s' => if string_dec x y then n else lku s' x
  end.
 
Fixpoint afu (s : env) (e : aexpr) : Z :=
  match e with
    anum n => n
  | avar x => lku s x
  | aplus e1 e2 => afu s e1 + afu s e2
  end.

Prouver par récurrence sur la dérivation de aeval r e v que l'on a la propriété suivante:

 
forall r e v, aeval r e v -> afu r e = v

A-t-on la réciproque ? C'est-à-dire :

forall r e v, afu r e = v -> aeval r e v

Gestion des erreurs

Pour permettre de distinguer les cas où le programme ne s'exécute pas correctement, on remplace les environnements par un type option. Si, à l'issue de l'évaluation correcte d'une expression, l'environnement est v, l'évaluateur d'expression renverra Some v, si l'évaluation amène une erreur, il renverra None.

Un tel évaluateur peut s'écrire :

Fixpoint afo (e : aexpr) (s : env) : option Z :=
  match e with
    anum n => Some n
  | avar x => lko s x
  | aplus e1 e2 =>
    match afo e1 s, afo e2 s with
      | Some u, Some v => Some (u + v)
      | _, _ => None
    end
  end.

Et la fonction de recherche dans l'environnement qui va avec :

Fixpoint lko (s : env) (x : string) : option Z :=
  match s with
   nil => None
  | (y, n)::s' => if string_dec x y then Some n else lko s' x
  end.

Prouver que l'on a maintenant bien : forall r e v, afo e r = Some v -> aeval r e v

Et maintenant, évaluons !

Écrire une fonction updf (x : string) (s : env) (v:Z) qui met remplace la valeur de x dans l'environnement s par v.

Écrire un évaluateur pour les fonctions booléennes, renvoyant un type option.

Écrire une fonction execf (r : env) (i:instr) (n:nat) qui renvoie Some s si à l'issue de l'exécution de l'instruction i s en n pas au plus, l'environnement est s, et None si l'exécution déclenche une erreur ou est incomplète.

Prouver la correction de votre évaluateur :

forall r i s, (exists n, execf (Some r) i n = Some r) <-> exec r i s