Ce module définit la syntaxe et la sémantique du langage IMP, un petit langage impératif structuré. Il illustre plusieurs styles de sémantiques.

Require Import Coq.Program.Equality. (* Pour faciliter certaines preuves. *)
Require Import List. (* La théorie des listes *)
Require Import Bool. (* La théorie des booléens *)
Require Import Arith. (* La théorie des entiers naturels (type nat) *)
Require Import ZArith. (* La théorie des entiers relatifs (type Z) *)
Require Import ZOdiv. (* Division entière avec arrondi vers zéro *)
Require Import Sequences. (* Une théorie des suites de transitions *)

Open Scope Z_scope. (* Interpréter +, -, etc, comme les opérations du type Z *)

1. Syntaxe abstraite

Les noms de variables sont identifiés par des entiers.

Definition ident : Type := Z.

Syntaxe des expressions arithmétiques, qui dénotent des entiers.

Syntaxe des expressions booléennes, qui dénotent soit true soit false. Utilisées comme conditions dans les commandes if et while.

Inductive bexp : Type :=
  | TRUE: bexp (* toujours vrai *)
  | FALSE: bexp (* toujours faux *)
  | Eq: aexp -> aexp -> bexp (* test d'égalité a1 == a2 *)
  | Le: aexp -> aexp -> bexp (* test plus petit ou égal a1 <= a2 *)
  | Not: bexp -> bexp (* négation !b *)
  | And: bexp -> bexp -> bexp. (* conjonction b1 & b2 *)

Syntaxe des commandes ("statements").

Inductive command : Type :=
  | Skip (* ne rien faire *)
  | Assign: ident -> aexp -> command (* affectation x = a; *)
  | Seq: command -> command -> command (* séquence c1; c2 *)
  | If: bexp -> command -> command -> command (* conditionnelle if (b) { c1 } else {c2} *)
  | While: bexp -> command -> command. (* boucle while (b) { c } *)

Un exemple de commande: la division euclidienne.

                      r = x;
                      q = 0;
                      while (y <= r) {
                          r = r - y;
                          q = q + 1;
                      }

Definition vx : ident := 1.
Definition vy : ident := 2.
Definition vq : ident := 3.
Definition vr : ident := 4.

Definition euclidean_division : command :=
  Seq (Assign vr (Var vx))
   (Seq (Assign vq (Const 0))
     (While (Le (Var vy) (Var vr))
       (Seq (Assign vr (Minus (Var vr) (Var vy)))
            (Assign vq (Plus (Var vq) (Const 1)))))).

2. Sémantique naturelle (big-step)

Représentation des états mémoire.

Un état mémoire associe à un nom de variable sa valeur entière (Some x) ou une valeur spéciale signifiant "variable non définie" (None).

Definition store : Type := ident -> option Z.

Dans l'état mémoire initial, toutes les variables sont non définies.

Definition initial_store : store := fun (x: ident) => None.

Mettre à jour la valeur d'une variable, sans changer les autres variables.

Definition update (x: ident) (val: Z) (m: store) : store :=
fun (y: ident) => if Z_eq_dec x y then Some val else m y.

Les propriétés "de bonnes variables" pour update.

Lemma update_same:
forall x val m, (update x val m) x = Some val.

Proof.

unfold update; intros. destruct (Z_eq_dec x x); congruence.
Qed.

Lemma update_other:
forall x val m y, x <> y -> (update x val m) y = m y.

Proof.

unfold update; intros. destruct (Z_eq_dec x y); congruence.
Qed.

Sémantique des expressions arithmétiques

eval m a n est vraie si l'expression a s'évalue en la valeur n dans l'état mémoire m, sans rencontrer d'erreurs. Les erreurs à l'exécution incluent:

faire référence à une variable qui n'a pas été initialisée
diviser par zéro.

Inductive eval: store -> aexp -> Z -> Prop :=
  | eval_const: forall m n,
      eval m (Const n) n
  | eval_var: forall m x n,
      m x = Some n ->
      eval m (Var x) n
  | eval_plus: forall m a1 a2 n1 n2,
      eval m a1 n1 -> eval m a2 n2 ->
      eval m (Plus a1 a2) (n1 + n2)
  | eval_minus: forall m a1 a2 n1 n2,
      eval m a1 n1 -> eval m a2 n2 ->
      eval m (Minus a1 a2) (n1 - n2)
  | eval_times: forall m a1 a2 n1 n2,
      eval m a1 n1 -> eval m a2 n2 ->
      eval m (Times a1 a2) (n1 * n2)
  | eval_div: forall m a1 a2 n1 n2,
      eval m a1 n1 -> eval m a2 n2 ->
      n2 <> 0 ->
      eval m (Div a1 a2) (n1 / n2).

Un exemple d'évaluation:

Goal eval (update vx 42 initial_store) (Plus (Var vx) (Const 2)) 44.

Proof.

  change 44 with (42 + 2). apply eval_plus.
  apply eval_var. apply update_same.
  apply eval_const.
Qed.

Deux exemples d'erreurs pendant l'évaluation:

Ltac inv H := inversion H; subst; clear H.

Goal forall n, ~(eval initial_store (Var vx) n).

Proof.

intros; red; intros. inv H. unfold initial_store in H2. congruence.
Qed.

Goal forall n, ~(eval initial_store (Div (Const 1) (Const 0)) n).

Proof.

intros; red; intros. inv H. inversion H4; subst. congruence.
Qed.

Exercice:

Modifier la sémantique pour faire en sorte qu'une erreur se produise dès qu'un résultat déborde de l'intervalle des entiers machine, disons de -32768 à 32767.

Sémantique des expressions booléennes

beval m be bv est vrai si l'expression booléenne be s'évalue en la valeur booléenne bv (soit true soit false) dans l'état mémoire m.

Inductive beval: store -> bexp -> bool -> Prop :=
  | beval_true: forall m,
      beval m TRUE true
  | beval_false: forall m,
      beval m FALSE false
  | beval_eq_true: forall m a1 a2 n1 n2,
      eval m a1 n1 -> eval m a2 n2 -> n1 = n2 ->
      beval m (Eq a1 a2) true
  | beval_eq_false: forall m a1 a2 n1 n2,
      eval m a1 n1 -> eval m a2 n2 -> n1 <> n2 ->
      beval m (Eq a1 a2) false
  | beval_le_true: forall m a1 a2 n1 n2,
      eval m a1 n1 -> eval m a2 n2 -> n1 <= n2 ->
      beval m (Le a1 a2) true
  | beval_le_false: forall m a1 a2 n1 n2,
      eval m a1 n1 -> eval m a2 n2 -> n1 > n2 ->
      beval m (Le a1 a2) false
  | beval_not: forall m be1 bv1,
      beval m be1 bv1 ->
      beval m (Not be1) (negb bv1)
  | beval_and: forall m be1 bv1 be2 bv2,
      beval m be1 bv1 -> beval m be2 bv2 ->
      beval m (And be1 be2) (bv1 && bv2).

Exercice:

Avec la sémantique ci-dessus, la conjonction And est "stricte" en ses deux arguments. Par exemple, false & 1 / 0 = 0 fait une erreur à l'exécution. Modifier la définition de beval pour que la conjonction And ne soit pas stricte en son second argument, comme l'opérateur && du C. Par exemple, false & 1 / 0 = 0 s'évaluerait en false.

Sémantique des commandes.

exec m c m' est vrai si la commande c, lancée dans l'état initial m, termine sans rencontrer d'erreurs dans l'état final m'.

Inductive exec: store -> command -> store -> Prop :=
  | exec_skip: forall m,
      exec m Skip m
  | exec_assign: forall m x a n,
      eval m a n ->
      exec m (Assign x a) (update x n m)
  | exec_seq: forall m c1 c2 m' m'',
      exec m c1 m' -> exec m' c2 m'' ->
      exec m (Seq c1 c2) m''
  | exec_if_true: forall m b ifso ifnot m',
      beval m b true -> exec m ifso m' ->
      exec m (If b ifso ifnot) m'
  | exec_if_false: forall m b ifso ifnot m',
      beval m b false -> exec m ifnot m' ->
      exec m (If b ifso ifnot) m'
  | exec_while_false: forall m b body,
      beval m b false ->
      exec m (While b body) m
  | exec_while_true: forall m b body m' m'',
      beval m b true -> exec m body m' -> exec m' (While b body) m'' ->
      exec m (While b body) m''.

Exemple d'exécution qui termine sans erreurs:

Goal let prog := If (Le (Const 1) (Const 2)) (Assign vx (Const 3)) (Assign vx (Const 0)) in
exists m, exec initial_store prog m /\ m vx = Some 3.

Proof.

  simpl. econstructor; split.
  apply exec_if_true. eapply beval_le_true. apply eval_const. apply eval_const. omega.
  eapply exec_assign. apply eval_const.
  apply update_same.
Qed.

Exemple d'exécution qui produit une erreur:

Goal let prog := Assign vx (Var vx) in
forall m, ~exec initial_store prog m.

Proof.

simpl; intros; red; intros. inv H. inv H4. unfold initial_store in H1. congruence.
Qed.

Exemple d'exécution qui ne termine pas:

Goal let prog := While TRUE Skip in
forall m m', ~exec m prog m'.

Proof.

simpl; intros; red; intros. dependent induction H. inv H. auto.
Qed.

3. Sémantique à transitions ("small-step" avec continuations)

La sémantique naturelle (comme le prédicat exec ci-dessus) est de type "à grands pas" ("big-step"): elle relie un terme (expression ou commande) au résultat final de son exécution (valeur, état mémoire final). C'est parfaitement adapté lorsque les exécutions terminent toujours, comme dans le cas des expressions arithmétiques et booléenne. Cependant, dans le cas des commandes, qui peuvent ne pas terminer, la sémantique naturelle ne décrit que les exécutions qui terminent. Elle ne permet pas de distinguer les exécutions qui "plantent" sur une erreur et les exécutions qui bouclent infiniment. Une alternative sont les sémantiques "à petits pas" ("small-step"), qui décomposent les exécutions en une suite d'étapes de calcul. Chaque étape représente l'exécution d'un calcul élémentaire, comme par exemple une affectation de variable. Partant du programme source et de l'état mémoire initial, nous construisons une suite d'étapes de calcul chaînées les unes après les autres. Trois comportements peuvent apparaître:

Terminaison sans erreur: après un nombre fini d'étapes, nous atteignons un état final, où le programme s'est entièrement exécuté.
Divergence: nous pouvons toujours effectuer une étape de calcul de plus, ce qui conduit à une suite infinie d'étapes.
Plantage sur une erreur: après un nombre fini d'étapes, nous atteignons un état qui n'est pas final et à partir duquel on ne peut effectuer aucune étape supplémentaire.

Un problème important dans les sémantiques "à petits pas" pour IMP est de savoir désigner la sous-commande du programme initial qui doit être exécutée à la prochaine étape. Autrement dit, il faut savoir parler de points de programmes. Par exemple, dans le programme x = 1; y = 2; la première étape doit désigner l'affectation x = 1 et l'exécuter. L'étape suivante se focalise sur y = 2 et l'exécute. Dans la sémantique à transitions ci-dessous, nous représentons le point de programme courant par une paire de:

une sous-commande du programme sur laquelle nous sommes focalisés;
un terme de continuation qui décrit ce qu'il reste à faire une fois que cette sous-commande a terminé.

Inductive continuation : Type :=
  | Kstop: continuation
  | Kseq: command -> continuation -> continuation
  | Kwhile: bexp -> command -> continuation -> continuation.

Intuitions:

Kstop signifie "fin du programme, l'exécution s'arrête"
Kseq c k signifie "exécuter la commande c, puis continuer avec k".
Kwhile b c k signifie "exécuter la boucle while (b) {c}, puis continuer avec k". C'est moralement équivalent à Kseq (While b c) k.

Exemples:

(Seq c1 c2, Kstop) représente le programme c1; c2
(c1, Kseq c2 Kstop) représente le même programme où on se focalise sur la sous-commande c1.

Les états d'exécution de la sémantique à transitions sont des triplets:

une sous-commande sur laquelle on est focalisé
son terme de continuation
l'état mémoire courant.

Definition state : Type := (command * continuation * store)%type.

La relation de transition ci-dessous, reliant deux états d'exécution, définit une étape élémentaire de calcul. On a trois familles de transitions:

Calculs: par exemple, exécuter une affectation, ou sélectionner une des deux branches d'un if
Focalisation: par exemple, dans la séquence c1;c2, on se focalise sur c1 et on sauvegarde c2 dans la continuation
Reprise: une fois que la commande focalisée s'est réduite en skip, on regarde la continuation pour savoir quoi faire ensuite.

Inductive step: state -> state -> Prop :=
  | step_assign: forall x e k m n, (* calcul *)
      eval m e n ->
      step (Assign x e, k, m)
           (Skip, k, update x n m)
  | step_seq: forall m c1 c2 k, (* focalisation *)
      step (Seq c1 c2, k, m)
           (c1, Kseq c2 k, m)
  | step_if_true: forall m b ifso ifnot k, (* calcul + focalisation *)
      beval m b true ->
      step (If b ifso ifnot, k, m)
           (ifso, k, m)
  | step_if_false: forall m b ifso ifnot k, (* calcul + focalisation *)
      beval m b false ->
      step (If b ifso ifnot, k, m)
           (ifnot, k, m)
  | step_while_false: forall m b body k, (* calcul *)
      beval m b false ->
      step (While b body, k, m)
           (Skip, k, m)
  | step_while_true: forall m b body k, (* calcul + focalisation *)
      beval m b true ->
      step (While b body, k, m)
           (body, Kwhile b body k, m)
  | step_skip_seq: forall c k m, (* reprise *)
      step (Skip, Kseq c k, m)
           (c, k, m)
  | step_skip_while: forall b body k m, (* reprise *)
      step (Skip, Kwhile b body k, m)
           (While b body, k, m).

Un programme termine sans erreurs s'il existe une suite finie de transitions

depuis l'état initial: commande = programme, continuation = Kstop, état mémoire = état mémoire initial
jusqu'à un état final: commande = Skip, continuation = Kstop.

Definition prog_terminates (prog: command) (m_final: store) : Prop :=
star step (prog, Kstop, initial_store) (Skip, Kstop, m_final).

Si R est une relation binaire, star R est sa fermeture réflexive et transitive. (Voir le module Sequences pour la définition.) star (transition C) step représente donc une suite de zéro, une ou plusieurs étapes de calcul.

Un programme diverge s'il existe une suite infinie de transitions à partir de l'état initial.

Definition prog_diverges (prog: command) : Prop :=
infseq step (prog, Kstop, initial_store).

De même, infseq R représente une suite infinie de transitions R. (Également défini dans le module Sequences.)

Enfin, un programme "plante" s'il existe une suite finie de transitions depuis l'état initial jusqu'à un état qui n'est pas final et qui ne peut pas faire de transitions.

Definition prog_crashes (prog: command) : Prop :=
  exists c, exists k, exists m,
      star step (prog, Kstop, initial_store) (c, k, m)
   /\ irred step (c, k, m)
   /\ ~(c = Skip /\ k = Kstop).

Exercice:

Ajouter au langage IMP les commandes break et continue de C. Écrire les règles de transitions appropriées pour exprimer la sémantique de break et continue. Que faut-il changer dans la sémantique naturelle?

4. Sémantiques à réductions ("small-step" sans continuations)

Un autre style de sémantiques "à petits pas" consiste simplement à réécrire progressivement le programme, chaque réécriture réduisant un calcul élémentaire. C'est souvent ce que l'on fait en mathématiques lorsqu'on calcule dans une expression arithmétique:

  (1 + 2) * (3 + 4) = 3 * (3 + 4) = 3 * 7 = 21

Nous illustrons ce style de sémantique sur les expressions arithmétiques du langage IMP. On commence par définir les réductions de tête: les réductions où l'on réécrit la tête d'une expression.

Inductive head_red (m: store): aexp -> aexp -> Prop :=
  | red_var: forall x n,
      m x = Some n ->
      head_red m (Var x) (Const n)
  | red_plus: forall n1 n2,
      head_red m (Plus (Const n1) (Const n2)) (Const (n1 + n2))
  | red_minus: forall n1 n2,
      head_red m (Minus (Const n1) (Const n2)) (Const (n1 - n2))
  | red_times: forall n1 n2,
      head_red m (Times (Const n1) (Const n2)) (Const (n1 * n2))
  | red_div: forall n1 n2,
      n2 <> 0 ->
      head_red m (Div (Const n1) (Const n2)) (Const (n1 / n2)).

Il ne suffit pas de savoir réduire en tête d'une expression: souvent, il faut aller chercher "en profondeur" une sous-expression qui est prête à se réduire. Par exemple, 3 + 4 se réduit en tête, mais pas (3 + 4) * 5. Dans cette dernière, il faut aller chercher la sous-expression (3 + 4), la réduire en tête en 7, et reconstruire l'expression réduite 7 * 5. Ceci s'appelle une réduction sous un contexte: la réduction de tête 3 + 4 --> 7 se produit sous le contexte ... * 5.

Nous représentons les contextes de réduction comme des fonctions des expressions dans les expressions. Par exemple, le contexte ... * 5 ci-dessus est représenté par la fonction fun a => Times(a, Const 5).

Definition context : Type := aexp -> aexp.

Toutes les fonctions du type aexp -> aexp ne sont pas des contextes valides pour la réduction. Par exemple, fun a => Const 42 n'est pas un contexte, car l'argument n'est pas utilisé. Moralement, il faut que la fonction représente un terme de type aexp avec un et un seul "trou", dans lequel elle insère son argument. Le prédicat inductif ci-dessous caractérise les fonctions qui sont des contextes valides.

Inductive iscontext: context -> Prop :=
  | iscontext_head:
      iscontext (fun x => x)
  | iscontext_plus_left: forall C a,
      iscontext C -> iscontext (fun x => Plus (C x) a)
  | iscontext_plus_right: forall C a,
      iscontext C -> iscontext (fun x => Plus a (C x))
  | iscontext_minus_left: forall C a,
      iscontext C -> iscontext (fun x => Minus (C x) a)
  | iscontext_minus_right: forall C a,
      iscontext C -> iscontext (fun x => Minus a (C x))
  | iscontext_times_left: forall C a,
      iscontext C -> iscontext (fun x => Times (C x) a)
  | iscontext_times_right: forall C a,
      iscontext C -> iscontext (fun x => Times a (C x))
  | iscontext_div_left: forall C a,
      iscontext C -> iscontext (fun x => Div (C x) a)
  | iscontext_div_right: forall C a,
      iscontext C -> iscontext (fun x => Div a (C x)).

Une étape de réduction consiste à:

décomposer l'expression courante en C a, où a est une sous-expression et C un contexte valide qui entoure a;
réduire a en tête, obtenant a';
reconstruire l'expression résiduelle C a' en mettant a' dans le contexte C.

Inductive red (m: store): aexp -> aexp -> Prop :=
  | red_context: forall C a a',
      head_red m a a' -> iscontext C ->
      red m (C a) (C a').

Par exemple, nous pouvons réduire (3 + 4) * 5 en utilisant le contexte C = fun x => Times x (Const 5).

Goal forall m,
red m (Times (Plus (Const 3) (Const 4)) (Const 5))
(Times (Const 7) (Const 5)).

Proof.

  intros. apply red_context with (C := fun x => Times x (Const 5)).
  apply red_plus.
  apply iscontext_times_left. apply iscontext_head.
Qed.

Une expression a s'évalue en l'entier n s'il existe une séquence finie de réductions de a vers Const n.

Definition eval' (m: store) (a: aexp) (n: Z) : Prop :=
star (red m) a (Const n).

5. Rendre la sémantique exécutable

Jusqu'ici, nous avons défini les sémantiques par des prédicats disant si oui ou non un certain terme s'évalue en un certain résultat. C'est très commode pour spécifier et pour raisonner sur les sémantiques, mais cela ne permet pas d'exécuter effectivement un programme.

Dans cette section, nous rendons la sémantique exécutable en la réécrivant sous forme de fonctions, effectivement calculables. Ces fonctions prennent un état mémoire et un terme syntaxique (expression, commande, etc) et retournent

ou bien None pour indiquer une erreur
ou bien Some r pour indiquer une exécution réussie qui produit le résultat r.

Une notation Coq très pratique pour propager les erreurs des sous-termes vers le terme tout entier.

Notation "'do' X <- A ; B" := (match A with Some X => B | None => None end)
(at level 200, X ident, A at level 100, B at level 200).

Évaluation d'une expression arithmétique: en cas de succès, renvoie la valeur entière de l'expression.

Fixpoint eval_f (m: store) (a: aexp) : option Z :=
  match a with
  | Const n => Some n
  | Var x => m x
  | Plus a1 a2 =>
      do n1 <- eval_f m a1; do n2 <- eval_f m a2; Some(n1 + n2)
  | Minus a1 a2 =>
      do n1 <- eval_f m a1; do n2 <- eval_f m a2; Some(n1 - n2)
  | Times a1 a2 =>
      do n1 <- eval_f m a1; do n2 <- eval_f m a2; Some(n1 * n2)
  | Div a1 a2 =>
      do n1 <- eval_f m a1; do n2 <- eval_f m a2;
      if Z_eq_dec n2 0 then None else Some(n1 / n2)
  end.

Trois exemples d'évaluation.

Compute (eval_f (update vx 42 initial_store) (Plus (Var vx) (Const 2))).
Compute (eval_f initial_store (Var vx)).
Compute (eval_f initial_store (Div (Const 1) (Const 0))).

Évaluation d'une expression booléenne.

Fixpoint beval_f (m: store) (be: bexp): option bool :=
  match be with
  | TRUE => Some true
  | FALSE => Some false
  | Eq a1 a2 =>
      do n1 <- eval_f m a1; do n2 <- eval_f m a2;
      Some(if Z_eq_dec n1 n2 then true else false)
  | Le a1 a2 =>
      do n1 <- eval_f m a1; do n2 <- eval_f m a2;
      Some(if Z_le_dec n1 n2 then true else false)
  | Not be1 =>
      do bv1 <- beval_f m be1; Some(negb bv1)
  | And be1 be2 =>
      do bv1 <- beval_f m be1; do bv2 <- beval_f m be2; Some(bv1 && bv2)
  end.

Exécution d'une transition de la sémantique à transitions et continuations.

Definition step_f (st: state) : option state :=
  match st with
  | (Assign x e, k, m) =>
      do n <- eval_f m e; Some (Skip, k, update x n m)
  | (Seq c1 c2, k, m) =>
      Some (c1, Kseq c2 k, m)
  | (If b ifso ifnot, k, m) =>
      do bv <- beval_f m b;
      Some ((if bv then ifso else ifnot), k, m)
  | (While b body, k, m) =>
      do bv <- beval_f m b;
      if bv then Some (body, Kwhile b body k, m) else Some (Skip, k, m)
  | (Skip, Kseq c k, m) =>
      Some (c, k, m)
  | (Skip, Kwhile b body k, m) =>
      Some (While b body, k, m)
  | _ =>
      None
  end.

On peut itérer step_f jusqu'à obtenir un état final ou une erreur. Cependant, toutes les fonctions Coq doivent terminer, et donc nous devons borner a priori le nombre d'itérations.

Inductive result : Type :=
  | Timeout: result
  | Error: result
  | Termination: store -> result.

Fixpoint steps_f (n: nat) (st: state) : result :=
  match n with
  | O => Timeout
  | S n' =>
      match st with
      | (Skip, Kstop, m) => Termination m
      | _ => match step_f st with None => Error | Some st' => steps_f n' st' end
      end
  end.

Definition run_prog (prog: command) : result := steps_f 100%nat (prog, Kstop, initial_store).

Quelques exemples d'exécution de programmes.

Compute (let prog := If (Le (Const 1) (Const 2)) (Assign vx (Const 3)) (Assign vx (Const 0)) in
         match run_prog prog with
         | Termination st => st vx
         | _ => None
         end).

Compute (let prog := Seq (Assign vx (Const 101)) (Seq (Assign vy (Const 7)) euclidean_division) in
         match run_prog prog with
         | Termination st => (st vq, st vr)
         | _ => (None, None)
         end).

Compute (let prog := Assign vx (Var vx) in
         run_prog prog).

Compute (let prog := While TRUE Skip in
         run_prog prog).

A. Annexe: preuves d'équivalences entre sémantiques

Sémantique naturelle -> sémantique à transitions.

Lemma exec_star_step:
forall m c m', exec m c m' -> forall k, star step (c, k, m) (Skip, k, m').

Proof.

  induction 1; intros.
  apply star_refl.
  apply star_one. constructor; auto.
  eapply star_step. constructor.
  eapply star_trans. apply IHexec1.
  eapply star_step. constructor.
  apply IHexec2.
  eapply star_step. apply step_if_true; auto. apply IHexec.
  eapply star_step. apply step_if_false; auto. apply IHexec.
  apply star_one. apply step_while_false; auto.
  eapply star_step. apply step_while_true; auto.
  eapply star_trans. apply IHexec1.
  eapply star_step. apply step_skip_while.
  apply IHexec2.
Qed.

Sémantique à transitions -> sémantique naturelle.

Inductive exec_cont: store -> continuation -> store -> Prop :=
  | exec_cont_stop: forall m,
      exec_cont m Kstop m
  | exec_cont_seq: forall c k m m' m'',
      exec m c m' -> exec_cont m' k m'' ->
      exec_cont m (Kseq c k) m''
  | exec_cont_while: forall b body k m m' m'',
      exec m (While b body) m' -> exec_cont m' k m'' ->
      exec_cont m (Kwhile b body k) m''.

Inductive exec_state: state -> store -> Prop :=
  | exec_state_intro: forall c k m m' m'',
      exec m c m' -> exec_cont m' k m'' ->
      exec_state (c, k, m) m''.

Lemma step_exec:
  forall s1 s2, step s1 s2 ->
  forall m_final, exec_state s2 m_final -> exec_state s1 m_final.

Proof.

  induction 1; intros m_final EX; inv EX.
  inv H4. econstructor. constructor; eauto. auto.
  inv H4. econstructor. econstructor; eauto. auto.
  econstructor. apply exec_if_true; eauto. auto.
  econstructor. apply exec_if_false; eauto. auto.
  inv H4. econstructor. apply exec_while_false; auto. auto.
  inv H5. econstructor. eapply exec_while_true; eauto. auto.
  econstructor. constructor. econstructor; eauto.
  econstructor. constructor. econstructor; eauto.
Qed.

Lemma star_step_exec:
forall s1 s2, star step s1 s2 ->
forall m_final, exec_state s2 m_final -> exec_state s1 m_final.

Proof.

induction 1; intros. auto. eapply step_exec; eauto.
Qed.

Equivalence entre sémantique naturelle et sémantique à transitions pour les programmes qui terminent.

Theorem prog_terminates_iff_exec:
forall prog m, prog_terminates prog m <-> exec initial_store prog m.

Proof.

  unfold prog_terminates; intros; split; intros.
  assert (exec_state (prog, Kstop, initial_store) m).
    eapply star_step_exec; eauto. econstructor. constructor. constructor.
  inv H0. inv H6. auto.
  apply exec_star_step; auto.
Qed.

Sémantique naturelle -> séquences de réductions.

Axiom extensionality:
forall (A B: Type) (f g: A -> B), (forall x, f x = g x) -> f = g.

Remark iscontext_compose:
forall C, iscontext C -> forall C', iscontext C' -> iscontext (fun x => C(C' x)).

Proof.

induction 1; intros; simpl; try (constructor; auto).
replace (fun x => C' x) with C'. auto. apply extensionality; auto.
Qed.

Remark red_under_context:
forall m C a a', red m a a' -> iscontext C -> red m (C a) (C a').

Proof.

intros. inv H. apply red_context with (C := fun x => C (C0 x)). auto.
apply iscontext_compose; auto.
Qed.

Remark star_red_under_context:
forall C m a a', star (red m) a a' -> iscontext C -> star (red m) (C a) (C a').

Proof.

induction 1; intros. constructor.
apply star_step with (C b). apply red_under_context; auto. auto.
Qed.

Lemma eval_star_red:
forall m a n, eval m a n -> star (red m) a (Const n).

Proof.

  induction 1.
  constructor.
  apply star_one. apply red_context with (C := fun x => x). constructor; auto. constructor.
  eapply star_trans.
  apply star_red_under_context with (C := fun x => Plus x a2). eauto.
  repeat constructor.
  eapply star_trans.
  apply star_red_under_context with (C := fun x => Plus (Const n1) x). eauto.
  repeat constructor.
  apply star_one. apply red_context with (C := fun x => x). constructor; auto. constructor.
  eapply star_trans.
  apply star_red_under_context with (C := fun x => Minus x a2). eauto.
  repeat constructor.
  eapply star_trans.
  apply star_red_under_context with (C := fun x => Minus (Const n1) x). eauto.
  repeat constructor.
  apply star_one. apply red_context with (C := fun x => x). constructor; auto. constructor.
  eapply star_trans.
  apply star_red_under_context with (C := fun x => Times x a2). eauto.
  repeat constructor.
  eapply star_trans.
  apply star_red_under_context with (C := fun x => Times (Const n1) x). eauto.
  repeat constructor.
  apply star_one. apply red_context with (C := fun x => x). constructor; auto. constructor.
  eapply star_trans.
  apply star_red_under_context with (C := fun x => Div x a2). eauto.
  repeat constructor.
  eapply star_trans.
  apply star_red_under_context with (C := fun x => Div (Const n1) x). eauto.
  repeat constructor.
  apply star_one. apply red_context with (C := fun x => x). constructor; auto. constructor.
Qed.

Séquences de réductions -> sémantique naturelle.

Lemma head_red_eval:
  forall m a a', head_red m a a' ->
  forall C, iscontext C ->
  forall n, eval m (C a') n -> eval m (C a) n.

Proof.

  induction 2; intros.
  inv H; inv H0; repeat constructor; auto.
  inv H1; constructor; auto.
  inv H1; constructor; auto.
  inv H1; constructor; auto.
  inv H1; constructor; auto.
  inv H1; constructor; auto.
  inv H1; constructor; auto.
  inv H1; constructor; auto.
  inv H1; constructor; auto.
Qed.

Lemma star_red_eval:
forall m a a', star (red m) a a' -> forall n, eval m a' n -> eval m a n.

Proof.

  induction 1; intros.
  auto.
  inv H. eapply head_red_eval; eauto.
Qed.

Equivalence entre sémantique naturelle et séquences de réductions pour les expressions arithmétiques.

Theorem aexp_eval_iff_eval':
forall m a n, eval m a n <-> eval' m a n.

Proof.

  unfold eval'. intros; split; intros.
  apply eval_star_red; auto.
  eapply star_red_eval; eauto. constructor.
Qed.

Sémantique exécutable -> sémantique relationnelle

Lemma eval_f_sound:
forall m a n, eval_f m a = Some n -> eval m a n.

Proof with

(try congruence).
  induction a; simpl; intros.
  inv H. constructor.
  constructor; auto.
  destruct (eval_f m a1) as []_eqn... destruct (eval_f m a2) as []_eqn... inv H; constructor; auto.
  destruct (eval_f m a1) as []_eqn... destruct (eval_f m a2) as []_eqn... inv H; constructor; auto.
  destruct (eval_f m a1) as []_eqn... destruct (eval_f m a2) as []_eqn... inv H; constructor; auto.
  destruct (eval_f m a1) as []_eqn... destruct (eval_f m a2) as []_eqn...
  destruct (Z_eq_dec z0 0)... inv H; constructor; auto.
Qed.

Lemma beval_f_sound:
forall m be bv, beval_f m be = Some bv -> beval m be bv.

Proof with

(try congruence).
  induction be; simpl; intros.
  inv H. constructor.
  inv H. constructor.
  destruct (eval_f m a) as []_eqn... destruct (eval_f m a0) as []_eqn... inv H.
  destruct (Z_eq_dec z z0); [eapply beval_eq_true|eapply beval_eq_false]; eauto; apply eval_f_sound; auto.
  destruct (eval_f m a) as []_eqn... destruct (eval_f m a0) as []_eqn... inv H.
  destruct (Z_le_dec z z0).
  eapply beval_le_true. apply eval_f_sound; eauto. apply eval_f_sound; eauto. auto.
  eapply beval_le_false. apply eval_f_sound; eauto. apply eval_f_sound; eauto. omega.
  destruct (beval_f m be)... inv H. constructor; auto.
  destruct (beval_f m be1)... destruct (beval_f m be2)... inv H. constructor; auto.
Qed.

Lemma step_f_sound:
forall st st', step_f st = Some st' -> step st st'.

Proof with

(try congruence).
  intros. destruct st as [[c1 k1] m1]. destruct st' as [[c2 k2] m2].
  destruct c1; simpl in H.
  destruct k1... inv H; constructor. inv H; constructor.
  destruct (eval_f m1 a) as []_eqn... inv H; constructor. eapply eval_f_sound; eauto.
  inv H; constructor.
  destruct (beval_f m1 b) as []_eqn... inv H.
  destruct b0; constructor; eapply beval_f_sound; eauto.
  destruct (beval_f m1 b) as []_eqn...
  destruct b0; inv H; constructor; eapply beval_f_sound; eauto.
Qed.

Sémantique relationnelle -> sémantique exécutable.

Lemma eval_f_complete:
forall m a n, eval m a n -> eval_f m a = Some n.

Proof.

  induction 1; simpl.
  auto.
  auto.
  rewrite IHeval1; rewrite IHeval2; auto.
  rewrite IHeval1; rewrite IHeval2; auto.
  rewrite IHeval1; rewrite IHeval2; auto.
  rewrite IHeval1; rewrite IHeval2. destruct (Z_eq_dec n2 0); congruence.
Qed.

Lemma beval_f_complete:
forall m be bv, beval m be bv -> beval_f m be = Some bv.

Proof.

  induction 1; simpl.
  auto.
  auto.
  rewrite (eval_f_complete _ _ _ H). rewrite (eval_f_complete _ _ _ H0).
  destruct (Z_eq_dec n1 n2); congruence.
  rewrite (eval_f_complete _ _ _ H). rewrite (eval_f_complete _ _ _ H0).
  destruct (Z_eq_dec n1 n2); congruence.
  rewrite (eval_f_complete _ _ _ H). rewrite (eval_f_complete _ _ _ H0).
  destruct (Z_le_dec n1 n2). auto. tauto.
  rewrite (eval_f_complete _ _ _ H). rewrite (eval_f_complete _ _ _ H0).
  destruct (Z_le_dec n1 n2); congruence.
  rewrite IHbeval; auto.
  rewrite IHbeval1; rewrite IHbeval2; auto.
Qed.

Lemma step_f_complete:
forall st st', step st st' -> step_f st = Some st'.

Proof.

  induction 1; simpl.
  rewrite (eval_f_complete _ _ _ H). auto.
  auto.
  rewrite (beval_f_complete _ _ _ H). auto.
  rewrite (beval_f_complete _ _ _ H). auto.
  rewrite (beval_f_complete _ _ _ H). auto.
  rewrite (beval_f_complete _ _ _ H). auto.
  auto.
  auto.
Qed.

Module IMP

1. Syntaxe abstraite

2. Sémantique naturelle (big-step)

Représentation des états mémoire.

Sémantique des expressions arithmétiques

Exercice:

Sémantique des expressions booléennes

Exercice:

Sémantique des commandes.

3. Sémantique à transitions ("small-step" avec continuations)

Exercice:

4. Sémantiques à réductions ("small-step" sans continuations)

5. Rendre la sémantique exécutable

A. Annexe: preuves d'équivalences entre sémantiques