Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 9d83a21e authored by MARCHE Claude's avatar MARCHE Claude

Hoare logic formalization proved up to seq rule

parent 6551fff6
theory Imp
(* identifiers *)
type ident
lemma ident_eq_dec : forall i1 i2:ident. i1=i2 \/ i1 <> i2
function mk_ident int : ident
axiom mk_ident_inj: forall i j:int. mk_ident i = mk_ident j -> i=j
(* expressions *)
type operator = Oplus | Ominus | Omult
type expr =
......@@ -12,6 +20,8 @@ type expr =
| Evar ident
| Ebin expr operator expr
(* statements *)
type stmt =
| Sskip
| Sassign ident expr
......@@ -22,11 +32,15 @@ type stmt =
lemma check_skip:
forall s:stmt. s=Sskip \/s<>Sskip
(* program states *)
use map.Map as IdMap
use import int.Int
type state = IdMap.map ident int
(* semantics of expressions *)
function eval_bin (x:int) (op:operator) (y:int) : int =
match op with
| Oplus -> x+y
......@@ -57,7 +71,7 @@ function eval_expr (s:state) (e:expr) : int =
eval_expr s (Ebin (Evar x) Oplus (Econst 13)) = 55
(* small-steps semantics *)
(* small-steps semantics for statements *)
inductive one_step state stmt state stmt =
......@@ -121,18 +135,26 @@ inductive one_step state stmt state stmt =
(* many steps of execution *)
inductive many_steps state stmt state stmt =
| many_steps_refl:
forall s1 s2:state, i1 i2:stmt. s1=s2 /\ i1=i2 -> many_steps s1 i1 s2 i2
forall s:state, i:stmt. many_steps s i s i
| many_steps_trans:
forall s1 s2 s3:state, i1 i2 i3:stmt.
one_step s1 i1 s2 i2 ->
many_steps s2 i2 s3 i3 ->
many_steps s1 i1 s3 i3
lemma many_steps_seq_rec:
forall s1 s3:state, i i3:stmt.
many_steps s1 i s3 i3 -> i3 = Sskip ->
forall i1 i2:stmt. i = Sseq i1 i2 ->
exists s2:state.
many_steps s1 i1 s2 Sskip /\ many_steps s2 i2 s3 Sskip
lemma many_steps_seq:
forall s1 s3:state, i i1 i2 i3:stmt.
many_steps s1 i s3 i3 -> i = Sseq i1 i2 -> i3 = Sskip ->
forall s1 s3:state, i1 i2:stmt [many_steps s1 (Sseq i1 i2) s3 Sskip].
many_steps s1 (Sseq i1 i2) s3 Sskip ->
exists s2:state.
many_steps s1 i1 s2 Sskip /\ many_steps s2 i2 s3 Sskip
......@@ -172,27 +194,21 @@ lemma eval_subst:
(* Hoare triples *)
type triple = T fmla stmt fmla
predicate valid_triple (t:triple) =
match t with
| T p i q ->
predicate valid_triple (p:fmla) (i:stmt) (q:fmla) =
forall s:state. eval_fmla s p ->
forall s':state. many_steps s i s' Sskip ->
eval_fmla s' q
end
(* Hoare logic rules *)
lemma assign_rule:
forall q:fmla, x:ident, e:expr.
valid_triple (T (subst q x e) (Sassign x e) q)
valid_triple (subst q x e) (Sassign x e) q
lemma seq_rule:
forall p q r:fmla, i1 i2:stmt.
valid_triple (T p i1 r) /\ valid_triple (T r i2 q) ->
valid_triple (T p (Sseq i1 i2) q)
valid_triple p i1 r /\ valid_triple r i2 q ->
valid_triple p (Sseq i1 i2) q
end
......
......@@ -100,6 +100,15 @@ Inductive many_steps : (map ident Z) -> stmt -> (map ident Z)
ident Z)) (i1:stmt) (i2:stmt) (i3:stmt), (one_step s1 i1 s2 i2) ->
((many_steps s2 i2 s3 i3) -> (many_steps s1 i1 s3 i3)).
Axiom many_steps_seq_rec : forall (s1:(map ident Z)) (s3:(map ident Z))
(i:stmt) (i3:stmt), (many_steps s1 i s3 i3) -> ((i3 = Sskip) ->
forall (i1:stmt) (i2:stmt), (i = (Sseq i1 i2)) -> exists s2:(map ident Z),
(many_steps s1 i1 s2 Sskip) /\ (many_steps s2 i2 s3 Sskip)).
Axiom many_steps_seq : forall (s1:(map ident Z)) (s3:(map ident Z)) (i1:stmt)
(i2:stmt), (many_steps s1 (Sseq i1 i2) s3 Sskip) -> exists s2:(map ident
Z), (many_steps s1 i1 s2 Sskip) /\ (many_steps s2 i2 s3 Sskip).
Inductive fmla :=
| Fterm : expr -> fmla .
......@@ -108,16 +117,6 @@ Definition eval_fmla(s:(map ident Z)) (f:fmla): Prop :=
| (Fterm e) => ~ ((eval_expr s e) = 0%Z)
end.
Inductive triple :=
| T : fmla -> stmt -> fmla -> triple .
Definition valid_triple(t:triple): Prop :=
match t with
| (T p i q) => forall (s:(map ident Z)), (eval_fmla s p) ->
forall (sqt:(map ident Z)), (many_steps s i sqt Sskip) ->
(eval_fmla sqt q)
end.
Parameter subst_expr: expr -> ident -> expr -> expr.
......@@ -130,6 +129,10 @@ Axiom subst_expr_def : forall (e:expr) (x:ident) (t:expr),
(subst_expr e2 x t)))
end.
Axiom eval_subst_expr : forall (s:(map ident Z)) (e:expr) (x:ident) (t:expr),
((eval_expr s (subst_expr e x t)) = (eval_expr (set s x (eval_expr s t))
e)).
Definition subst(f:fmla) (x:ident) (t:expr): fmla :=
match f with
| (Fterm e) => (Fterm (subst_expr e x t))
......@@ -138,12 +141,16 @@ Definition subst(f:fmla) (x:ident) (t:expr): fmla :=
Axiom eval_subst : forall (s:(map ident Z)) (f:fmla) (x:ident) (t:expr),
(eval_fmla s (subst f x t)) -> (eval_fmla (set s x (eval_expr s t)) f).
Definition valid_triple(p:fmla) (i:stmt) (q:fmla): Prop := forall (s:(map
ident Z)), (eval_fmla s p) -> forall (sqt:(map ident Z)), (many_steps s i
sqt Sskip) -> (eval_fmla sqt q).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem assign_rule : forall (q:fmla) (x:ident) (e:expr),
(valid_triple (T (subst q x e) (Sassign x e) q)).
(valid_triple (subst q x e) (Sassign x e) q).
(* YOU MAY EDIT THE PROOF BELOW *)
intros q x e.
unfold valid_triple.
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter ident : Type.
Parameter mk_ident: Z -> ident.
Inductive operator :=
| Oplus : operator
| Ominus : operator
| Omult : operator .
Inductive expr :=
| Econst : Z -> expr
| Evar : ident -> expr
| Ebin : expr -> operator -> expr -> expr .
Inductive stmt :=
| Sskip : stmt
| Sassign : ident -> expr -> stmt
| Sseq : stmt -> stmt -> stmt
| Sif : expr -> stmt -> stmt -> stmt
| Swhile : expr -> stmt -> stmt .
Axiom check_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition state := (map ident Z).
Definition eval_bin(x:Z) (op:operator) (y:Z): Z :=
match op with
| Oplus => (x + y)%Z
| Ominus => (x - y)%Z
| Omult => (x * y)%Z
end.
Set Implicit Arguments.
Fixpoint eval_expr(s:(map ident Z)) (e:expr) {struct e}: Z :=
match e with
| (Econst n) => n
| (Evar x) => (get s x)
| (Ebin e1 op e2) => (eval_bin (eval_expr s e1) op (eval_expr s e2))
end.
Unset Implicit Arguments.
Inductive one_step : (map ident Z) -> stmt -> (map ident Z)
-> stmt -> Prop :=
| one_step_assign : forall (s:(map ident Z)) (x:ident) (e:expr),
(one_step s (Sassign x e) (set s x (eval_expr s e)) Sskip)
| one_step_seq : forall (s:(map ident Z)) (sqt:(map ident Z)) (i1:stmt)
(i1qt:stmt) (i2:stmt), (one_step s i1 sqt i1qt) -> (one_step s (Sseq i1
i2) sqt (Sseq i1qt i2))
| one_step_seq_skip : forall (s:(map ident Z)) (i:stmt), (one_step s
(Sseq Sskip i) s i)
| one_step_if_true : forall (s:(map ident Z)) (e:expr) (i1:stmt) (i2:stmt),
(~ ((eval_expr s e) = 0%Z)) -> (one_step s (Sif e i1 i2) s i1)
| one_step_if_false : forall (s:(map ident Z)) (e:expr) (i1:stmt)
(i2:stmt), ((eval_expr s e) = 0%Z) -> (one_step s (Sif e i1 i2) s i2)
| one_step_while_true : forall (s:(map ident Z)) (e:expr) (i:stmt),
(~ ((eval_expr s e) = 0%Z)) -> (one_step s (Swhile e i) s (Sseq i
(Swhile e i)))
| one_step_while_false : forall (s:(map ident Z)) (e:expr) (i:stmt),
((eval_expr s e) = 0%Z) -> (one_step s (Swhile e i) s Sskip).
Axiom progress : forall (s:(map ident Z)) (i:stmt), (~ (i = Sskip)) ->
exists sqt:(map ident Z), exists iqt:stmt, (one_step s i sqt iqt).
Inductive many_steps : (map ident Z) -> stmt -> (map ident Z)
-> stmt -> Prop :=
| many_steps_refl : forall (s:(map ident Z)) (i:stmt), (many_steps s i s i)
| many_steps_trans : forall (s1:(map ident Z)) (s2:(map ident Z)) (s3:(map
ident Z)) (i1:stmt) (i2:stmt) (i3:stmt), (one_step s1 i1 s2 i2) ->
((many_steps s2 i2 s3 i3) -> (many_steps s1 i1 s3 i3)).
Axiom many_steps_seq : forall (s1:(map ident Z)) (s3:(map ident Z)) (i1:stmt)
(i2:stmt), (many_steps s1 (Sseq i1 i2) s3 Sskip) -> exists s2:(map ident
Z), (many_steps s1 i1 s2 Sskip) /\ (many_steps s2 i2 s3 Sskip).
Inductive fmla :=
| Fterm : expr -> fmla .
Definition eval_fmla(s:(map ident Z)) (f:fmla): Prop :=
match f with
| (Fterm e) => ~ ((eval_expr s e) = 0%Z)
end.
Parameter subst_expr: expr -> ident -> expr -> expr.
Axiom subst_expr_def : forall (e:expr) (x:ident) (t:expr),
match e with
| (Econst _) => ((subst_expr e x t) = e)
| (Evar y) => ((x = y) -> ((subst_expr e x t) = t)) /\ ((~ (x = y)) ->
((subst_expr e x t) = e))
| (Ebin e1 op e2) => ((subst_expr e x t) = (Ebin (subst_expr e1 x t) op
(subst_expr e2 x t)))
end.
Axiom eval_subst_expr : forall (s:(map ident Z)) (e:expr) (x:ident) (t:expr),
((eval_expr s (subst_expr e x t)) = (eval_expr (set s x (eval_expr s t))
e)).
Definition subst(f:fmla) (x:ident) (t:expr): fmla :=
match f with
| (Fterm e) => (Fterm (subst_expr e x t))
end.
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem eval_subst : forall (s:(map ident Z)) (f:fmla) (x:ident) (t:expr),
(eval_fmla s (subst f x t)) -> (eval_fmla (set s x (eval_expr s t)) f).
(* YOU MAY EDIT THE PROOF BELOW *)
induction f; unfold eval_fmla, subst in *.
intros x t H.
rewrite <- eval_subst_expr; auto.
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter ident : Type.
Axiom ident_eq_dec : forall (i1:ident) (i2:ident), (i1 = i2) \/ ~ (i1 = i2).
Parameter mk_ident: Z -> ident.
Axiom mk_ident_inj : forall (i:Z) (j:Z), ((mk_ident i) = (mk_ident j)) ->
(i = j).
Inductive operator :=
| Oplus : operator
| Ominus : operator
| Omult : operator .
Inductive expr :=
| Econst : Z -> expr
| Evar : ident -> expr
| Ebin : expr -> operator -> expr -> expr .
Inductive stmt :=
| Sskip : stmt
| Sassign : ident -> expr -> stmt
| Sseq : stmt -> stmt -> stmt
| Sif : expr -> stmt -> stmt -> stmt
| Swhile : expr -> stmt -> stmt .
Axiom check_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition state := (map ident Z).
Definition eval_bin(x:Z) (op:operator) (y:Z): Z :=
match op with
| Oplus => (x + y)%Z
| Ominus => (x - y)%Z
| Omult => (x * y)%Z
end.
Set Implicit Arguments.
Fixpoint eval_expr(s:(map ident Z)) (e:expr) {struct e}: Z :=
match e with
| (Econst n) => n
| (Evar x) => (get s x)
| (Ebin e1 op e2) => (eval_bin (eval_expr s e1) op (eval_expr s e2))
end.
Unset Implicit Arguments.
Inductive one_step : (map ident Z) -> stmt -> (map ident Z)
-> stmt -> Prop :=
| one_step_assign : forall (s:(map ident Z)) (x:ident) (e:expr),
(one_step s (Sassign x e) (set s x (eval_expr s e)) Sskip)
| one_step_seq : forall (s:(map ident Z)) (sqt:(map ident Z)) (i1:stmt)
(i1qt:stmt) (i2:stmt), (one_step s i1 sqt i1qt) -> (one_step s (Sseq i1
i2) sqt (Sseq i1qt i2))
| one_step_seq_skip : forall (s:(map ident Z)) (i:stmt), (one_step s
(Sseq Sskip i) s i)
| one_step_if_true : forall (s:(map ident Z)) (e:expr) (i1:stmt) (i2:stmt),
(~ ((eval_expr s e) = 0%Z)) -> (one_step s (Sif e i1 i2) s i1)
| one_step_if_false : forall (s:(map ident Z)) (e:expr) (i1:stmt)
(i2:stmt), ((eval_expr s e) = 0%Z) -> (one_step s (Sif e i1 i2) s i2)
| one_step_while_true : forall (s:(map ident Z)) (e:expr) (i:stmt),
(~ ((eval_expr s e) = 0%Z)) -> (one_step s (Swhile e i) s (Sseq i
(Swhile e i)))
| one_step_while_false : forall (s:(map ident Z)) (e:expr) (i:stmt),
((eval_expr s e) = 0%Z) -> (one_step s (Swhile e i) s Sskip).
Axiom progress : forall (s:(map ident Z)) (i:stmt), (~ (i = Sskip)) ->
exists sqt:(map ident Z), exists iqt:stmt, (one_step s i sqt iqt).
Inductive many_steps : (map ident Z) -> stmt -> (map ident Z)
-> stmt -> Prop :=
| many_steps_refl : forall (s:(map ident Z)) (i:stmt), (many_steps s i s i)
| many_steps_trans : forall (s1:(map ident Z)) (s2:(map ident Z)) (s3:(map
ident Z)) (i1:stmt) (i2:stmt) (i3:stmt), (one_step s1 i1 s2 i2) ->
((many_steps s2 i2 s3 i3) -> (many_steps s1 i1 s3 i3)).
Axiom many_steps_seq_rec : forall (s1:(map ident Z)) (s3:(map ident Z))
(i:stmt) (i3:stmt), (many_steps s1 i s3 i3) -> ((i3 = Sskip) ->
forall (i1:stmt) (i2:stmt), (i = (Sseq i1 i2)) -> exists s2:(map ident Z),
(many_steps s1 i1 s2 Sskip) /\ (many_steps s2 i2 s3 Sskip)).
Axiom many_steps_seq : forall (s1:(map ident Z)) (s3:(map ident Z)) (i1:stmt)
(i2:stmt), (many_steps s1 (Sseq i1 i2) s3 Sskip) -> exists s2:(map ident
Z), (many_steps s1 i1 s2 Sskip) /\ (many_steps s2 i2 s3 Sskip).
Inductive fmla :=
| Fterm : expr -> fmla .
Definition eval_fmla(s:(map ident Z)) (f:fmla): Prop :=
match f with
| (Fterm e) => ~ ((eval_expr s e) = 0%Z)
end.
Parameter subst_expr: expr -> ident -> expr -> expr.
Axiom subst_expr_def : forall (e:expr) (x:ident) (t:expr),
match e with
| (Econst _) => ((subst_expr e x t) = e)
| (Evar y) => ((x = y) -> ((subst_expr e x t) = t)) /\ ((~ (x = y)) ->
((subst_expr e x t) = e))
| (Ebin e1 op e2) => ((subst_expr e x t) = (Ebin (subst_expr e1 x t) op
(subst_expr e2 x t)))
end.
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem eval_subst_expr : forall (s:(map ident Z)) (e:expr) (x:ident)
(t:expr), ((eval_expr s (subst_expr e x t)) = (eval_expr (set s x
(eval_expr s t)) e)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros s e x t.
induction e.
(* case Econst *)
rewrite (subst_expr_def (Econst z) x t).
now simpl.
(* case Evar *)
generalize (subst_expr_def (Evar i) x t).
intros (H1,H2).
case (ident_eq_dec x i).
(* subcase x=i *)
simpl; intro; subst x.
rewrite Select_eq; auto.
now rewrite H1.
(* subcase x<>i *)
simpl; intro.
rewrite Select_neq; auto.
now rewrite H2.
(* case Ebin *)
rewrite (subst_expr_def (Ebin e1 o e2) x t).
simpl.
rewrite IHe2.
now rewrite IHe1.
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter ident : Type.
Parameter mk_ident: Z -> ident.
Inductive operator :=
| Oplus : operator
| Ominus : operator
| Omult : operator .
Inductive expr :=
| Econst : Z -> expr
| Evar : ident -> expr
| Ebin : expr -> operator -> expr -> expr .
Inductive stmt :=
| Sskip : stmt
| Sassign : ident -> expr -> stmt
| Sseq : stmt -> stmt -> stmt
| Sif : expr -> stmt -> stmt -> stmt
| Swhile : expr -> stmt -> stmt .
Axiom check_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition state := (map ident Z).
Definition eval_bin(x:Z) (op:operator) (y:Z): Z :=
match op with
| Oplus => (x + y)%Z
| Ominus => (x - y)%Z
| Omult => (x * y)%Z
end.
Set Implicit Arguments.
Fixpoint eval_expr(s:(map ident Z)) (e:expr) {struct e}: Z :=
match e with
| (Econst n) => n
| (Evar x) => (get s x)
| (Ebin e1 op e2) => (eval_bin (eval_expr s e1) op (eval_expr s e2))
end.
Unset Implicit Arguments.
Inductive one_step : (map ident Z) -> stmt -> (map ident Z)
-> stmt -> Prop :=
| one_step_assign : forall (s:(map ident Z)) (x:ident) (e:expr),
(one_step s (Sassign x e) (set s x (eval_expr s e)) Sskip)
| one_step_seq : forall