Library coq_chap_08_SOS



Require Import Bool Arith List.
Import List.ListNotations.

Préliminaires

Syntaxe des expressions arithmétiques


Inductive aexp :=
| Aco : nat → aexp
constantes
| Ava : nat → aexp
variables
| Apl : aexp → aexp → aexp
| Amu : aexp → aexp → aexp
| Amo : aexp → aexp → aexp
.

Syntaxe des expressions booléennes


Inductive bexp :=
| Btrue : bexp
| Bfalse : bexp
| Bnot : bexp → bexp
| Band : bexp → bexp → bexp
| Bor : bexp → bexp → bexp
| Beq : bexp → bexp → bexp
| Beqnat : aexp → aexp → bexp
.

Syntaxe du langage impératif WHILE


Inductive winstr :=
| : winstr
| Assign : nat → aexp → winstr
| Seq : winstr → winstr → winstr
| If : bexp → winstr → winstr → winstr
| While : bexp → winstr → winstr
.

États


Definition state := list nat.

Fixpoint get (x:nat) (s:state) : nat :=
match x,s with
| 0 , v::_ ⇒ v
| S x1, _::l1 ⇒ get x1 l1
| _ , _ ⇒ 0
end.

Fixpoint update (s:state) (v:nat) (n:nat): state :=
match v,s with
| 0 , a :: l1 ⇒ n :: l1
| 0 , nil ⇒ n :: nil
| S v1, a :: l1 ⇒ a :: (update l1 v1 n)
| S v1, nil ⇒ 0 :: (update nil v1 n)
end.

Sémantique fonctionnelle de aexp et de bexp


Fixpoint evalA (a: aexp) (s: state) : nat :=
  match a with
  | Aco n ⇒ n
  | Ava x ⇒ get x s
  | Apl a1 a2 ⇒ evalA a1 s + evalA a2 s
  | Amu a1 a2 ⇒ evalA a1 s × evalA a2 s
  | Amo a1 a2 ⇒ evalA a1 s - evalA a2 s
  end.

Definition eqboolb b1 b2 : bool :=
  match b1, b2 with
  | true , true ⇒ true
  | false, false ⇒ true
  | _ , _ ⇒ false
  end.

Fixpoint eqnatb n1 n2 : bool :=
  match n1, n2 with
  | O , O ⇒ true
  | S n1', S n2' ⇒ eqnatb n1' n2'
  | _ , _ ⇒ false
  end.

Fixpoint evalB (b : bexp) (s : state) : bool :=
  match b with
  | Btrue ⇒ true
  | Bfalse ⇒ false
  | Bnot b ⇒ negb (evalB b s)
  | Band e1 e2 ⇒ (evalB e1 s) && (evalB e2 s)
  | Bor e1 e2 ⇒ (evalB e1 s) || (evalB e2 s)
  | Beq e1 e2 ⇒ eqboolb (evalB e1 s) (evalB e2 s)
  | Beqnat n1 n2 ⇒ eqnatb (evalA n1 s) (evalA n2 s)
  end.

La SN de WHILE, pour comparaison avec sa SOS


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


SOS (Sémantique opérationnelle à petits pas) du langage While


Inductive config :=
| Inter : winstr → state → config
| Final : state → config.


Inductive SOS_1: winstr → state → config → Prop :=
| SOS_Skip : ∀ s,
                 SOS_1 Skip s (Final s)

| SOS_Assign : ∀ x a s,
                 SOS_1 (Assign x a) s (Final (update s x (evalA a s)))

| SOS_Seqf : ∀ i1 i2 s s1,
                 SOS_1 i1 s (Final s1) →
                 SOS_1 (Seq i1 i2) s (Inter i2 s1)
| SOS_Seqi : ∀ i1 i1' i2 s s1,
                 SOS_1 i1 s (Inter i1' s1) →
                 SOS_1 (Seq i1 i2) s (Inter (Seq i1' i2) s1)


| SOS_If_true : ∀ b i1 i2 s,
                 evalB b s = true →
                 SOS_1 (If b i1 i2) s (Inter i1 s)
| SOS_If_false : ∀ b i1 i2 s,
                 evalB b s = false →
                 SOS_1 (If b i1 i2) s (Inter i2 s)



| SOS_While : ∀ b i s,
                 SOS_1 (While b i) s (Inter (If b (Seq i (While b i)) Skip) s)
.

Fermeture réflexive-transitive de SOS_1 Cette sémantique donne toutes les configurations atteignables par un (AST de) programme en partant d'un état initial.

Inductive SOS : config → config → Prop :=
| SOS_stop : ∀ c, SOS c c
| SOS_again : ∀ i1 s1 c2 c3,
              SOS_1 i1 s1 c2 → SOS c2 c3 →
              SOS (Inter i1 s1) c3.

Tests


Definition N0 := Aco 0.
Definition N1 := Aco 1.
Definition N2 := Aco 2.
Definition N3 := Aco 3.
Definition N4 := Aco 4.

On code dans WHILE un programme P1 correspondant à while not (i=0) do {i:=i-1;x:=1+x}
Definition Il := 0.
Definition Ir := Ava Il.
Definition Xl := 1.
Definition Xr := Ava Xl.

Definition corps_boucle := Seq (Assign Il (Amo Ir N1)) (Assign Xl (Apl N1 Xr)).
Definition P1 := While (Bnot (Beqnat Ir N0)) corps_boucle.

Configuration obtenue par SOS_1 depuis P1

Theorem SOS_1_P1 :
  SOS_1 P1 [1; 2]
   (Inter
     (If (Bnot (Beqnat Ir N0))
         (Seq corps_boucle P1)
         Skip)
     [1; 2]).
Proof.
  unfold P1.
  apply SOS_While.
Qed.

Configuration obtenue par 1 pas de SOS depuis P1

Theorem experience_1_pas :
  SOS (Inter P1 [1; 2])
   (Inter
     (If (Bnot (Beqnat Ir N0))
         (Seq corps_boucle P1)
         Skip)
     [1; 2]).
Proof.
  unfold P1.
  eapply SOS_again.
  { apply SOS_While. }
  apply SOS_stop.
Qed.

À partir de la configuration composée de P1 et de l'état 1; 2, la SOS permet d'atteindre une configuration finale d'état 0; 3

Theorem experience_tous_les_pas : SOS (Inter P1 [1; 2]) (Final [0; 3]).
Proof.
  unfold P1.
  eapply SOS_again.
  { apply SOS_While. }
  eapply SOS_again.
  { apply SOS_If_true. cbn. reflexivity. }
  eapply SOS_again.
  { unfold corps_boucle. eapply SOS_Seqi.
    eapply SOS_Seqf. apply SOS_Assign. }
  cbn. eapply SOS_again.
  { eapply SOS_Seqf. apply SOS_Assign. }
  cbn. eapply SOS_again.
  { apply SOS_While. }
  eapply SOS_again.
  { apply SOS_If_false. cbn. reflexivity. }
  eapply SOS_again.
  { apply SOS_Skip. }
  apply SOS_stop.
Qed.