223 lines
7.9 KiB
Coq
223 lines
7.9 KiB
Coq
(* Projet Coq - WP - MPRI 2.7.1 *)
|
|
|
|
(***** Partie 1 : definition de While ****************************************)
|
|
|
|
Require Import ZArith.BinInt.
|
|
Import Z.
|
|
|
|
Definition Var := nat.
|
|
Definition Mem := Var -> Z.
|
|
Definition Expr:= Mem -> Z.
|
|
|
|
Inductive Instr : Type :=
|
|
| skip: Instr
|
|
| abort: Instr
|
|
| assign: Var -> Expr -> Instr
|
|
| seq: Instr -> Instr -> Instr
|
|
| ifelse: Expr -> Instr -> Instr -> Instr
|
|
| while: Expr -> Instr -> Instr.
|
|
|
|
Definition ifonly (exp: Expr) (inst: Instr) : Instr :=
|
|
ifelse exp inst skip.
|
|
|
|
(***** CPO *******************************************************************)
|
|
|
|
Fixpoint nat_eq x y :=
|
|
match x, y with
|
|
| 0, 0 => true
|
|
| 0, S _ => false
|
|
| S _, 0 => false
|
|
| S x0, S y0 => nat_eq x0 y0
|
|
end.
|
|
|
|
Definition Sequence (S: Type) := nat -> S.
|
|
|
|
Inductive cpo (T: Type): Type :=
|
|
| CpoError: (cpo T)
|
|
| CpoElem: T -> (cpo T).
|
|
|
|
Definition cpo_leq: forall (T: Type), cpo T -> cpo T -> Prop :=
|
|
fun T x y => match x, y with
|
|
| CpoError _, _ => True
|
|
| CpoElem _ x0, CpoElem _ y0 => x0 = y0
|
|
| _, _ => False
|
|
end.
|
|
Arguments cpo_leq {T} _ _.
|
|
Infix "cpo<=" := cpo_leq (at level 100).
|
|
|
|
Definition is_chain: forall (T: Type), Sequence (cpo T) -> Prop :=
|
|
fun T chain => forall (n: nat), (chain n) cpo<= (chain (S n)).
|
|
Arguments is_chain {T} _.
|
|
|
|
Definition is_lub_of: forall (T: Type), Sequence (cpo T) -> cpo T -> Prop :=
|
|
fun T chain elt => forall (n: nat), (chain n) cpo<= elt.
|
|
Arguments is_lub_of {T} _ _.
|
|
|
|
Axiom find_lub: forall (T: Type), Sequence (cpo T) -> cpo T.
|
|
Arguments find_lub {T} _.
|
|
|
|
Axiom find_lub_correct:
|
|
forall (T: Type), forall (chain: Sequence (cpo T)),
|
|
is_chain chain -> is_lub_of chain (find_lub chain).
|
|
Arguments find_lub_correct {T} {chain} _.
|
|
|
|
(***** Interpretation ********************************************************)
|
|
|
|
Definition subst: Mem -> Var -> Z -> Mem :=
|
|
fun (m: Mem) (v: Var) (z: Z) (v2: Var) =>
|
|
if nat_eq v v2 then z else m v2.
|
|
Notation "m [ x <- z ]" := (subst m x z) (at level 50, left associativity).
|
|
|
|
Definition MemCpo := cpo Mem.
|
|
Definition MemError := CpoError Mem.
|
|
Definition MemElem := CpoElem Mem.
|
|
|
|
Fixpoint interp (inst: Instr) (mem: MemCpo) : MemCpo :=
|
|
match mem with
|
|
| CpoError _ => MemError
|
|
| CpoElem _ mem0 =>
|
|
match inst with
|
|
| skip => MemElem mem0
|
|
| abort => MemError
|
|
| assign v e => (MemElem (mem0 [v <- (e mem0)]))
|
|
| seq instr1 instr2 => interp instr2 (interp instr1 (MemElem mem0))
|
|
| ifelse guard instrIf instrElse =>
|
|
if ((guard mem0) =? 0) % Z
|
|
then interp instrIf mem
|
|
else interp instrElse mem
|
|
| while guard body =>
|
|
let fix while_chain (mem: MemCpo) (n: nat): MemCpo :=
|
|
match n with
|
|
| 0 => mem
|
|
| S m =>
|
|
match while_chain (MemElem mem0) m with
|
|
| CpoError _ => MemError
|
|
| CpoElem _ submem =>
|
|
if ((guard submem) =? 0) % Z
|
|
then interp body (MemElem submem)
|
|
else mem
|
|
end
|
|
end
|
|
in find_lub (fun n =>
|
|
match while_chain (MemElem mem0) n with
|
|
| CpoError _ => MemError
|
|
| CpoElem _ submem =>
|
|
if ((guard submem) =? 0) % Z
|
|
then MemError
|
|
else MemElem submem
|
|
end)
|
|
end
|
|
end.
|
|
|
|
(***** Validite, prouvabilite pour Hoare *************************************)
|
|
|
|
Definition Assert := Mem -> Prop.
|
|
Delimit Scope assert with assert.
|
|
|
|
Definition assertTop : Assert := fun _ => True.
|
|
Definition assertBot : Assert := fun _ => False.
|
|
|
|
Definition assertNot : Assert -> Assert :=
|
|
fun orig mem => ~ (orig mem).
|
|
Notation "~ x" := (assertNot x) (at level 75, right associativity) : assert.
|
|
Definition assertAnd : Assert -> Assert -> Assert :=
|
|
fun x1 x2 mem => (x1 mem) /\ (x2 mem).
|
|
Infix "/\" := assertAnd : assert.
|
|
Definition assertOr : Assert -> Assert -> Assert :=
|
|
fun x1 x2 mem => (x1 mem) \/ (x2 mem).
|
|
Infix "\/" := assertOr : assert.
|
|
Definition assertImpl : Assert -> Assert -> Assert :=
|
|
fun x1 x2 => (~x1 \/ x2) % assert.
|
|
Infix "->" := assertImpl : assert.
|
|
Definition assertForall : Var -> Assert -> Assert :=
|
|
fun ident asser mem => forall (z: Z), asser (mem [ident <- z]).
|
|
Notation "\-/ x" := (assertForall x) (at level 90, no associativity) : assert.
|
|
Definition existsForall : Var -> Assert -> Assert :=
|
|
fun ident asser mem => exists (z: Z), asser (mem [ident <- z]).
|
|
Notation "'exists' x" := (existsForall x)
|
|
(at level 87, no associativity): assert.
|
|
Definition assertMemForall : Assert -> Assert :=
|
|
fun asser mem => forall (mem: Mem), asser mem.
|
|
Notation "'\-/m' x" := (assertMemForall x)
|
|
(at level 90, no associativity): assert.
|
|
Definition existsMemForall : Assert -> Assert :=
|
|
fun asser mem => exists (mem: Mem), asser mem.
|
|
Notation "'exists_m' x" := (existsMemForall x)
|
|
(at level 87, no associativity): assert.
|
|
|
|
Definition substAssert : Assert -> Var -> Z -> Assert :=
|
|
fun asser ident val mem => asser (mem [ident <- val]).
|
|
Notation "a [[ x <- z ]]" := (substAssert a x z)
|
|
(at level 50, left associativity).
|
|
Definition substAssertExpr : Assert -> Var -> Expr -> Assert :=
|
|
fun asser ident expr mem => asser (mem [ident <- (expr mem)]).
|
|
Notation "a [[ x <- 'expr' z ]]" := (substAssertExpr a x z)
|
|
(at level 50, left associativity).
|
|
|
|
Definition assertOfExpr : Expr -> Assert :=
|
|
fun expr mem => expr mem <> 0%Z.
|
|
|
|
Definition assertImplLogical : Assert -> Assert -> Prop :=
|
|
fun a1 a2 => forall (m : Mem), (a1 m) -> (a2 m).
|
|
|
|
|
|
(***** Hoare provability *****************************************************)
|
|
|
|
Parameter hoare_provability : Assert -> Instr -> Assert -> Prop.
|
|
Notation "|- [| pre |] instr [| post |]" :=
|
|
(hoare_provability pre instr post) (at level 30): assert.
|
|
|
|
Axiom h_skip: forall (asser: Assert), ( |- [|asser|] skip [|asser|]) % assert.
|
|
Axiom h_abort: forall (a1:Assert), forall (a2: Assert),
|
|
(|- [|a1|] abort [|a2|]) % assert.
|
|
Axiom h_assign: forall (asser: Assert), forall (x: Var), forall (e: Expr),
|
|
(|- [| asser [[ x <- expr e ]] |] (assign x e) [|asser|]) % assert.
|
|
Axiom h_conseq:
|
|
forall (a1: Assert), forall (a1': Assert),
|
|
forall (a2: Assert), forall (a2': Assert),
|
|
forall (s: Instr),
|
|
(|- [| a1' |] s [| a2' |]) % assert ->
|
|
(assertImplLogical a1 a1') ->
|
|
(assertImplLogical a2' a2) ->
|
|
(|- [| a1 |] s [| a2 |]) % assert.
|
|
Axiom h_seq:
|
|
forall (a1: Assert), forall (a2: Assert), forall (a3: Assert),
|
|
forall (s1: Instr), forall (s2: Instr),
|
|
(|- [|a1|] s1 [|a2|]) % assert -> (|- [|a2|] s2 [|a3|]) % assert ->
|
|
(|- [|a1|] (seq s1 s2) [|a3|]) % assert.
|
|
Axiom h_if:
|
|
forall (a1: Assert), forall (a2: Assert),
|
|
forall (e: Expr),
|
|
forall (s1: Instr), forall (s2: Instr),
|
|
(|- [| a1 /\ (assertOfExpr e) |] s1 [| a2 |]) % assert ->
|
|
(|- [| a1 /\ ~ (assertOfExpr e) |] s2 [| a2 |]) % assert ->
|
|
(|- [| a1 |] (ifelse e s1 s2) [| a2 |]) % assert.
|
|
Axiom h_while:
|
|
forall (inv: Assert),
|
|
forall (e: Expr),
|
|
forall (s: Instr),
|
|
(|- [| inv /\ (assertOfExpr e) |] s [| inv |]) % assert ->
|
|
(|- [| inv |] (while e s) [| inv /\ ~ (assertOfExpr e) |]) % assert.
|
|
|
|
(***** Hoare: provability implies consequence ********************************)
|
|
|
|
Definition conseq_or_bottom (y: Assert) (m: MemCpo) :=
|
|
match m with
|
|
| CpoError _ => True
|
|
| CpoElem _ m0 => y m0
|
|
end.
|
|
|
|
Definition hoare_consequence (pre: Assert) (instr: Instr) (post: Assert) :=
|
|
forall mem: Mem,
|
|
(pre mem) -> (conseq_or_bottom post (interp instr (MemElem mem))).
|
|
|
|
Notation "|= [| pre |] instr [| post |]" :=
|
|
(hoare_consequence pre instr post) (at level 30): assert.
|
|
|
|
Theorem hoare_provability_implies_consequence :
|
|
forall (pre: Assert), forall (s: Instr), forall (post: Assert),
|
|
( |- [| pre |] s [| post |] ) % assert
|
|
-> ( |= [| pre |] s [| post |] ) % assert.
|
|
Proof.
|
|
(* TODO *)
|
|
Admitted.
|