Reindent consistently bullets
This commit is contained in:
parent
5dfc412c10
commit
908bed1331
1 changed files with 277 additions and 275 deletions
552
wp.v
552
wp.v
|
|
@ -19,17 +19,17 @@ Inductive Instr : Type :=
|
||||||
| while: Expr -> Instr -> Instr.
|
| while: Expr -> Instr -> Instr.
|
||||||
|
|
||||||
Definition ifonly (exp: Expr) (inst: Instr) : Instr :=
|
Definition ifonly (exp: Expr) (inst: Instr) : Instr :=
|
||||||
ifelse exp inst skip.
|
ifelse exp inst skip.
|
||||||
|
|
||||||
(***** CPO *******************************************************************)
|
(***** CPO *******************************************************************)
|
||||||
|
|
||||||
Fixpoint nat_eq x y :=
|
Fixpoint nat_eq x y :=
|
||||||
match x, y with
|
match x, y with
|
||||||
| 0, 0 => true
|
| 0, 0 => true
|
||||||
| 0, S _ => false
|
| 0, S _ => false
|
||||||
| S _, 0 => false
|
| S _, 0 => false
|
||||||
| S x0, S y0 => nat_eq x0 y0
|
| S x0, S y0 => nat_eq x0 y0
|
||||||
end.
|
end.
|
||||||
|
|
||||||
Definition Sequence (S: Type) := nat -> S.
|
Definition Sequence (S: Type) := nat -> S.
|
||||||
|
|
||||||
|
|
@ -38,35 +38,35 @@ Inductive cpo (T: Type): Type :=
|
||||||
| CpoElem: T -> (cpo T).
|
| CpoElem: T -> (cpo T).
|
||||||
|
|
||||||
Definition cpo_leq: forall (T: Type), cpo T -> cpo T -> Prop :=
|
Definition cpo_leq: forall (T: Type), cpo T -> cpo T -> Prop :=
|
||||||
fun T x y => match x, y with
|
fun T x y => match x, y with
|
||||||
| CpoError _, _ => True
|
| CpoError _, _ => True
|
||||||
| CpoElem _ x0, CpoElem _ y0 => x0 = y0
|
| CpoElem _ x0, CpoElem _ y0 => x0 = y0
|
||||||
| _, _ => False
|
| _, _ => False
|
||||||
end.
|
end.
|
||||||
Arguments cpo_leq {T} _ _.
|
Arguments cpo_leq {T} _ _.
|
||||||
Infix "cpo<=" := cpo_leq (at level 100).
|
Infix "cpo<=" := cpo_leq (at level 100).
|
||||||
|
|
||||||
Definition is_chain: forall (T: Type), Sequence (cpo T) -> Prop :=
|
Definition is_chain: forall (T: Type), Sequence (cpo T) -> Prop :=
|
||||||
fun T chain => forall (n: nat), (chain n) cpo<= (chain (S n)).
|
fun T chain => forall (n: nat), (chain n) cpo<= (chain (S n)).
|
||||||
Arguments is_chain {T} _.
|
Arguments is_chain {T} _.
|
||||||
|
|
||||||
Definition is_lub_of: forall (T: Type), Sequence (cpo T) -> cpo T -> Prop :=
|
Definition is_lub_of: forall (T: Type), Sequence (cpo T) -> cpo T -> Prop :=
|
||||||
fun T chain elt => forall (n: nat), (chain n) cpo<= elt.
|
fun T chain elt => forall (n: nat), (chain n) cpo<= elt.
|
||||||
Arguments is_lub_of {T} _ _.
|
Arguments is_lub_of {T} _ _.
|
||||||
|
|
||||||
Axiom find_lub: forall (T: Type), Sequence (cpo T) -> cpo T.
|
Axiom find_lub: forall (T: Type), Sequence (cpo T) -> cpo T.
|
||||||
Arguments find_lub {T} _.
|
Arguments find_lub {T} _.
|
||||||
|
|
||||||
Axiom find_lub_correct:
|
Axiom find_lub_correct:
|
||||||
forall (T: Type), forall (chain: Sequence (cpo T)),
|
forall (T: Type), forall (chain: Sequence (cpo T)),
|
||||||
is_chain chain -> is_lub_of chain (find_lub chain).
|
is_chain chain -> is_lub_of chain (find_lub chain).
|
||||||
Arguments find_lub_correct {T} {chain} _.
|
Arguments find_lub_correct {T} {chain} _.
|
||||||
|
|
||||||
(***** Interpretation ********************************************************)
|
(***** Interpretation ********************************************************)
|
||||||
|
|
||||||
Definition subst: Mem -> Var -> Z -> Mem :=
|
Definition subst: Mem -> Var -> Z -> Mem :=
|
||||||
fun (m: Mem) (v: Var) (z: Z) (v2: Var) =>
|
fun (m: Mem) (v: Var) (z: Z) (v2: Var) =>
|
||||||
if nat_eq v v2 then z else m v2.
|
if nat_eq v v2 then z else m v2.
|
||||||
Notation "m [ x <- z ]" := (subst m x z) (at level 50, left associativity).
|
Notation "m [ x <- z ]" := (subst m x z) (at level 50, left associativity).
|
||||||
|
|
||||||
Definition MemCpo := cpo Mem.
|
Definition MemCpo := cpo Mem.
|
||||||
|
|
@ -74,47 +74,47 @@ Definition MemError := CpoError Mem.
|
||||||
Definition MemElem := CpoElem Mem.
|
Definition MemElem := CpoElem Mem.
|
||||||
|
|
||||||
Fixpoint interp (inst: Instr) (mem: MemCpo) : MemCpo :=
|
Fixpoint interp (inst: Instr) (mem: MemCpo) : MemCpo :=
|
||||||
match mem with
|
match mem with
|
||||||
| CpoError _ => MemError
|
| CpoError _ => MemError
|
||||||
| CpoElem _ mem0 =>
|
| CpoElem _ mem0 =>
|
||||||
match inst with
|
match inst with
|
||||||
| skip => MemElem mem0
|
| skip => MemElem mem0
|
||||||
| abort => MemError
|
| abort => MemError
|
||||||
| assign v e => (MemElem (mem0 [v <- (e mem0)]))
|
| assign v e => (MemElem (mem0 [v <- (e mem0)]))
|
||||||
| seq instr1 instr2 => interp instr2 (interp instr1 (MemElem mem0))
|
| seq instr1 instr2 => interp instr2 (interp instr1 (MemElem mem0))
|
||||||
| ifelse guard instrIf instrElse =>
|
| ifelse guard instrIf instrElse =>
|
||||||
if ((guard mem0) =? 0) % Z
|
if ((guard mem0) =? 0) % Z
|
||||||
then interp instrElse mem
|
then interp instrElse mem
|
||||||
else interp instrIf mem
|
else interp instrIf mem
|
||||||
| while guard body =>
|
| while guard body =>
|
||||||
let fix while_chain (mem: MemCpo) (n: nat): MemCpo :=
|
let fix while_chain (mem: MemCpo) (n: nat): MemCpo :=
|
||||||
match n with
|
match n with
|
||||||
| 0 => mem
|
| 0 => mem
|
||||||
| S m =>
|
| S m =>
|
||||||
match while_chain (MemElem mem0) m with
|
match while_chain (MemElem mem0) m with
|
||||||
| CpoError _ => MemError
|
| CpoError _ => MemError
|
||||||
| CpoElem _ submem =>
|
| CpoElem _ submem =>
|
||||||
if ((guard submem) =? 0) % Z
|
if ((guard submem) =? 0) % Z
|
||||||
then interp body (MemElem submem)
|
then interp body (MemElem submem)
|
||||||
else mem
|
else mem
|
||||||
end
|
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
|
||||||
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.
|
||||||
|
|
||||||
Fixpoint nth_iterate (instr: Instr) (n: nat) : Instr :=
|
Fixpoint nth_iterate (instr: Instr) (n: nat) : Instr :=
|
||||||
match n with
|
match n with
|
||||||
| 0 => skip
|
| 0 => skip
|
||||||
| S m => seq (nth_iterate instr m) instr
|
| S m => seq (nth_iterate instr m) instr
|
||||||
end.
|
end.
|
||||||
|
|
||||||
Definition satisfies_expr (mem: MemCpo) (expr: Expr) : Prop := match mem with
|
Definition satisfies_expr (mem: MemCpo) (expr: Expr) : Prop := match mem with
|
||||||
| CpoError _ => False
|
| CpoError _ => False
|
||||||
|
|
@ -123,40 +123,40 @@ end.
|
||||||
Infix "|=e" := satisfies_expr (at level 32).
|
Infix "|=e" := satisfies_expr (at level 32).
|
||||||
|
|
||||||
Definition expr_neg (expr: Expr) : Expr :=
|
Definition expr_neg (expr: Expr) : Expr :=
|
||||||
fun mem => match expr mem with
|
fun mem => match expr mem with
|
||||||
| 0%Z => 1%Z
|
| 0%Z => 1%Z
|
||||||
| _ => 0%Z
|
| _ => 0%Z
|
||||||
end.
|
end.
|
||||||
|
|
||||||
Lemma certain_termination_exists body guard mem :
|
Lemma certain_termination_exists body guard mem :
|
||||||
interp (while guard body) mem <> MemError ->
|
interp (while guard body) mem <> MemError ->
|
||||||
exists n: nat,
|
exists n: nat,
|
||||||
interp (nth_iterate (ifonly guard body) n) mem |=e expr_neg guard.
|
interp (nth_iterate (ifonly guard body) n) mem |=e expr_neg guard.
|
||||||
Proof.
|
Proof.
|
||||||
intros noError.
|
intros noError.
|
||||||
Admitted.
|
Admitted.
|
||||||
|
|
||||||
Lemma certain_termination_exists_minimal body guard mem :
|
Lemma certain_termination_exists_minimal body guard mem :
|
||||||
interp (while guard body) mem <> MemError ->
|
interp (while guard body) mem <> MemError ->
|
||||||
exists n: nat,
|
exists n: nat,
|
||||||
(forall p: nat, p < n ->
|
(forall p: nat, p < n ->
|
||||||
interp (nth_iterate (ifonly guard body) p) mem |=e guard)
|
interp (nth_iterate (ifonly guard body) p) mem |=e guard)
|
||||||
/\ interp (nth_iterate (ifonly guard body) n) mem |=e expr_neg guard.
|
/\ interp (nth_iterate (ifonly guard body) n) mem |=e expr_neg guard.
|
||||||
Proof.
|
Proof.
|
||||||
intros not_error.
|
intros not_error.
|
||||||
Admitted.
|
Admitted.
|
||||||
|
|
||||||
Lemma certain_termination body guard mem :
|
Lemma certain_termination body guard mem :
|
||||||
interp (while guard body) mem <> MemError ->
|
interp (while guard body) mem <> MemError ->
|
||||||
exists n: nat,
|
exists n: nat,
|
||||||
(interp (nth_iterate body n) mem) |=e (expr_neg guard)
|
(interp (nth_iterate body n) mem) |=e (expr_neg guard)
|
||||||
/\ (forall p, p < n -> (interp (nth_iterate body p) mem) |=e guard)
|
/\ (forall p, p < n -> (interp (nth_iterate body p) mem) |=e guard)
|
||||||
/\ interp (while guard body) mem = interp (nth_iterate body n) mem.
|
/\ interp (while guard body) mem = interp (nth_iterate body n) mem.
|
||||||
Proof.
|
Proof.
|
||||||
intros notError.
|
intros notError.
|
||||||
elim (certain_termination_exists_minimal body guard mem).
|
elim (certain_termination_exists_minimal body guard mem).
|
||||||
intros n. intros [notBeforeN atN]. exists n.
|
intros n. intros [notBeforeN atN]. exists n.
|
||||||
split.
|
split.
|
||||||
Admitted.
|
Admitted.
|
||||||
|
|
||||||
(***** Validite, prouvabilite pour Hoare *************************************)
|
(***** Validite, prouvabilite pour Hoare *************************************)
|
||||||
|
|
@ -168,47 +168,47 @@ Definition assertTop : Assert := fun _ => True.
|
||||||
Definition assertBot : Assert := fun _ => False.
|
Definition assertBot : Assert := fun _ => False.
|
||||||
|
|
||||||
Definition assertNot : Assert -> Assert :=
|
Definition assertNot : Assert -> Assert :=
|
||||||
fun orig mem => ~ (orig mem).
|
fun orig mem => ~ (orig mem).
|
||||||
Notation "~ x" := (assertNot x) (at level 75, right associativity) : assert.
|
Notation "~ x" := (assertNot x) (at level 75, right associativity) : assert.
|
||||||
Definition assertAnd : Assert -> Assert -> Assert :=
|
Definition assertAnd : Assert -> Assert -> Assert :=
|
||||||
fun x1 x2 mem => (x1 mem) /\ (x2 mem).
|
fun x1 x2 mem => (x1 mem) /\ (x2 mem).
|
||||||
Infix "/\" := assertAnd : assert.
|
Infix "/\" := assertAnd : assert.
|
||||||
Definition assertOr : Assert -> Assert -> Assert :=
|
Definition assertOr : Assert -> Assert -> Assert :=
|
||||||
fun x1 x2 mem => (x1 mem) \/ (x2 mem).
|
fun x1 x2 mem => (x1 mem) \/ (x2 mem).
|
||||||
Infix "\/" := assertOr : assert.
|
Infix "\/" := assertOr : assert.
|
||||||
Definition assertImpl : Assert -> Assert -> Assert :=
|
Definition assertImpl : Assert -> Assert -> Assert :=
|
||||||
fun x1 x2 => (~x1 \/ x2) % assert.
|
fun x1 x2 => (~x1 \/ x2) % assert.
|
||||||
Infix "->" := assertImpl : assert.
|
Infix "->" := assertImpl : assert.
|
||||||
Definition assertForall : Var -> Assert -> Assert :=
|
Definition assertForall : Var -> Assert -> Assert :=
|
||||||
fun ident asser mem => forall (z: Z), asser (mem [ident <- z]).
|
fun ident asser mem => forall (z: Z), asser (mem [ident <- z]).
|
||||||
Notation "\-/ x" := (assertForall x) (at level 90, no associativity) : assert.
|
Notation "\-/ x" := (assertForall x) (at level 90, no associativity) : assert.
|
||||||
Definition existsForall : Var -> Assert -> Assert :=
|
Definition existsForall : Var -> Assert -> Assert :=
|
||||||
fun ident asser mem => exists (z: Z), asser (mem [ident <- z]).
|
fun ident asser mem => exists (z: Z), asser (mem [ident <- z]).
|
||||||
Notation "'exists' x" := (existsForall x)
|
Notation "'exists' x" := (existsForall x)
|
||||||
(at level 87, no associativity): assert.
|
(at level 87, no associativity): assert.
|
||||||
Definition assertMemForall : Assert -> Assert :=
|
Definition assertMemForall : Assert -> Assert :=
|
||||||
fun asser mem => forall (mem: Mem), asser mem.
|
fun asser mem => forall (mem: Mem), asser mem.
|
||||||
Notation "'\-/m' x" := (assertMemForall x)
|
Notation "'\-/m' x" := (assertMemForall x)
|
||||||
(at level 90, no associativity): assert.
|
(at level 90, no associativity): assert.
|
||||||
Definition existsMemForall : Assert -> Assert :=
|
Definition existsMemForall : Assert -> Assert :=
|
||||||
fun asser mem => exists (mem: Mem), asser mem.
|
fun asser mem => exists (mem: Mem), asser mem.
|
||||||
Notation "'exists_m' x" := (existsMemForall x)
|
Notation "'exists_m' x" := (existsMemForall x)
|
||||||
(at level 87, no associativity): assert.
|
(at level 87, no associativity): assert.
|
||||||
|
|
||||||
Definition substAssert : Assert -> Var -> Z -> Assert :=
|
Definition substAssert : Assert -> Var -> Z -> Assert :=
|
||||||
fun asser ident val mem => asser (mem [ident <- val]).
|
fun asser ident val mem => asser (mem [ident <- val]).
|
||||||
Notation "a [[ x <- z ]]" := (substAssert a x z)
|
Notation "a [[ x <- z ]]" := (substAssert a x z)
|
||||||
(at level 50, left associativity).
|
(at level 50, left associativity).
|
||||||
Definition substAssertExpr : Assert -> Var -> Expr -> Assert :=
|
Definition substAssertExpr : Assert -> Var -> Expr -> Assert :=
|
||||||
fun asser ident expr mem => asser (mem [ident <- (expr mem)]).
|
fun asser ident expr mem => asser (mem [ident <- (expr mem)]).
|
||||||
Notation "a [[ x <- 'expr' z ]]" := (substAssertExpr a x z)
|
Notation "a [[ x <- 'expr' z ]]" := (substAssertExpr a x z)
|
||||||
(at level 50, left associativity).
|
(at level 50, left associativity).
|
||||||
|
|
||||||
Definition assertOfExpr : Expr -> Assert :=
|
Definition assertOfExpr : Expr -> Assert :=
|
||||||
fun expr mem => (expr mem <> 0)%Z.
|
fun expr mem => (expr mem <> 0)%Z.
|
||||||
|
|
||||||
Definition assertImplLogical (a1 a2: Assert): Prop :=
|
Definition assertImplLogical (a1 a2: Assert): Prop :=
|
||||||
forall (m: Mem), (a1 m) -> (a2 m).
|
forall (m: Mem), (a1 m) -> (a2 m).
|
||||||
|
|
||||||
|
|
||||||
(***** Hoare provability *****************************************************)
|
(***** Hoare provability *****************************************************)
|
||||||
|
|
@ -216,248 +216,250 @@ Definition assertImplLogical (a1 a2: Assert): Prop :=
|
||||||
Reserved Notation "|- [| x |] y [| z |]" (at level 30).
|
Reserved Notation "|- [| x |] y [| z |]" (at level 30).
|
||||||
|
|
||||||
Inductive hoare_provability : Assert -> Instr -> Assert -> Prop :=
|
Inductive hoare_provability : Assert -> Instr -> Assert -> Prop :=
|
||||||
| H_skip: forall pre, hoare_provability pre skip pre
|
| H_skip: forall pre, hoare_provability pre skip pre
|
||||||
| H_abort: forall pre, forall post, hoare_provability pre abort post
|
| H_abort: forall pre, forall post, hoare_provability pre abort post
|
||||||
| H_assign: forall post, forall (x: Var), forall (e: Expr),
|
| H_assign: forall post, forall (x: Var), forall (e: Expr),
|
||||||
(|- [| post [[ x <- expr e ]] |] (assign x e) [| post |]) % assert
|
(|- [| post [[ x <- expr e ]] |] (assign x e) [| post |]) % assert
|
||||||
| H_conseq:
|
| H_conseq:
|
||||||
forall pre, forall post,
|
forall pre, forall post,
|
||||||
forall pre', forall post',
|
forall pre', forall post',
|
||||||
forall s,
|
forall s,
|
||||||
|
(|- [| pre' |] s [| post' |]) % assert ->
|
||||||
(|- [| pre' |] s [| post' |]) % assert ->
|
(assertImplLogical pre pre') ->
|
||||||
(assertImplLogical pre pre') ->
|
(assertImplLogical post' post) ->
|
||||||
(assertImplLogical post' post) ->
|
(|- [| pre |] s [| post |]) % assert
|
||||||
(|- [| pre |] s [| post |]) % assert
|
| H_seq:
|
||||||
| H_seq:
|
forall pre, forall mid, forall post, forall s1, forall s2,
|
||||||
forall pre, forall mid, forall post, forall s1, forall s2,
|
(|- [|pre|] s1 [|mid|]) % assert ->
|
||||||
(|- [|pre|] s1 [|mid|]) % assert ->
|
(|- [|mid|] s2 [|post|]) % assert ->
|
||||||
(|- [|mid|] s2 [|post|]) % assert ->
|
(|- [|pre|] (seq s1 s2) [|post|]) % assert
|
||||||
(|- [|pre|] (seq s1 s2) [|post|]) % assert
|
| H_if:
|
||||||
| H_if:
|
forall pre, forall post, forall expr, forall sIf, forall sElse,
|
||||||
forall pre, forall post, forall expr, forall sIf, forall sElse,
|
(|- [| pre /\ (assertOfExpr expr) |] sIf [| post |]) % assert ->
|
||||||
(|- [| pre /\ (assertOfExpr expr) |] sIf [| post |]) % assert ->
|
(|- [| pre /\ ~(assertOfExpr expr) |] sElse [| post |]) % assert ->
|
||||||
(|- [| pre /\ ~(assertOfExpr expr) |] sElse [| post |]) % assert ->
|
(|- [| pre |] (ifelse expr sIf sElse) [| post |]) % assert
|
||||||
(|- [| pre |] (ifelse expr sIf sElse) [| post |]) % assert
|
| H_while:
|
||||||
| H_while:
|
forall inv, forall expr, forall sBody,
|
||||||
forall inv, forall expr, forall sBody,
|
(|- [| inv /\ (assertOfExpr expr) |] sBody [| inv |]) % assert ->
|
||||||
(|- [| inv /\ (assertOfExpr expr) |] sBody [| inv |]) % assert ->
|
(|- [| inv |] (while expr sBody)
|
||||||
(|- [| inv |] (while expr sBody)
|
[| inv /\ ~ (assertOfExpr expr) |]) % assert
|
||||||
[| inv /\ ~ (assertOfExpr expr) |]) % assert
|
|
||||||
where "|- [| pre |] instr [| post |]" :=
|
where "|- [| pre |] instr [| post |]" :=
|
||||||
(hoare_provability pre instr post) : assert.
|
(hoare_provability pre instr post) : assert.
|
||||||
|
|
||||||
(***** Hoare: provability implies consequence ********************************)
|
(***** Hoare: provability implies consequence ********************************)
|
||||||
|
|
||||||
Definition conseq_or_bottom (y: Assert) (m: MemCpo) :=
|
Definition conseq_or_bottom (y: Assert) (m: MemCpo) :=
|
||||||
match m with
|
match m with
|
||||||
| CpoError _ => True
|
| CpoError _ => True
|
||||||
| CpoElem _ m0 => y m0
|
| CpoElem _ m0 => y m0
|
||||||
end.
|
end.
|
||||||
|
|
||||||
Definition hoare_consequence (pre: Assert) (instr: Instr) (post: Assert) :=
|
Definition hoare_consequence (pre: Assert) (instr: Instr) (post: Assert) :=
|
||||||
forall mem: Mem,
|
forall mem: Mem,
|
||||||
(pre mem) -> (conseq_or_bottom post (interp instr (MemElem mem))).
|
(pre mem) -> (conseq_or_bottom post (interp instr (MemElem mem))).
|
||||||
|
|
||||||
Notation "|= [| pre |] instr [| post |]" :=
|
Notation "|= [| pre |] instr [| post |]" :=
|
||||||
(hoare_consequence pre instr post) (at level 30): assert.
|
(hoare_consequence pre instr post) (at level 30): assert.
|
||||||
|
|
||||||
Lemma weaken_in_conseq:
|
Lemma weaken_in_conseq:
|
||||||
forall a1, forall a2, forall m,
|
forall a1, forall a2, forall m,
|
||||||
assertImplLogical a1 a2 -> conseq_or_bottom a1 m ->
|
assertImplLogical a1 a2 -> conseq_or_bottom a1 m ->
|
||||||
conseq_or_bottom a2 m.
|
conseq_or_bottom a2 m.
|
||||||
Proof.
|
Proof.
|
||||||
intros a1 a2 m impl conseq. destruct m.
|
intros a1 a2 m impl conseq. destruct m.
|
||||||
- apply conseq.
|
- apply conseq.
|
||||||
- simpl. unfold assertImplLogical in impl. apply (impl m). apply conseq.
|
- simpl. unfold assertImplLogical in impl. apply (impl m). apply conseq.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Lemma interp_of_error (s: Instr):
|
Lemma interp_of_error (s: Instr):
|
||||||
interp s (MemError) = MemError.
|
interp s (MemError) = MemError.
|
||||||
Proof.
|
Proof.
|
||||||
unfold MemError. destruct s; cbv; trivial.
|
unfold MemError. destruct s; cbv; trivial.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Lemma conseq_or_bottom_is_conseq (y: Assert) (m: Mem) :
|
Lemma conseq_or_bottom_is_conseq (y: Assert) (m: Mem) :
|
||||||
conseq_or_bottom y (MemElem m) -> y m.
|
conseq_or_bottom y (MemElem m) -> y m.
|
||||||
Proof.
|
Proof.
|
||||||
intros src; unfold conseq_or_bottom; simpl; trivial.
|
intros src; unfold conseq_or_bottom; simpl; trivial.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Lemma unfold_one_iter (s: Instr) (m: Mem) (n: nat):
|
Lemma unfold_one_iter (s: Instr) (m: Mem) (n: nat):
|
||||||
interp (nth_iterate s (S n)) (MemElem m)
|
interp (nth_iterate s (S n)) (MemElem m)
|
||||||
= interp s (interp (nth_iterate s n) (MemElem m)).
|
= interp s (interp (nth_iterate s n) (MemElem m)).
|
||||||
Proof.
|
Proof.
|
||||||
simpl; congruence.
|
simpl; congruence.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Lemma error_leads_to_no_success s:
|
Lemma error_leads_to_no_success s:
|
||||||
forall m, interp s MemError <> MemElem m.
|
forall m, interp s MemError <> MemElem m.
|
||||||
Proof.
|
Proof.
|
||||||
intros mem. unfold interp; destruct s; simpl ;
|
intros mem. unfold interp; destruct s; simpl ;
|
||||||
unfold MemElem; unfold MemError; congruence.
|
unfold MemElem; unfold MemError; congruence.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Lemma expr_neg_consistency (expr: Expr):
|
Lemma expr_neg_consistency (expr: Expr):
|
||||||
forall mem, expr_neg expr mem <> 0%Z -> (~ assertOfExpr expr)%assert mem.
|
forall mem, expr_neg expr mem <> 0%Z -> (~ assertOfExpr expr)%assert mem.
|
||||||
Proof.
|
Proof.
|
||||||
intros mem. intros src.
|
intros mem. intros src.
|
||||||
unfold assertNot. unfold assertOfExpr. destruct (expr mem) eqn:exprRel.
|
unfold assertNot. unfold assertOfExpr. destruct (expr mem) eqn:exprRel.
|
||||||
+ congruence.
|
+ congruence.
|
||||||
+ elimtype False.
|
+ elimtype False.
|
||||||
unfold expr_neg in src; rewrite exprRel in src. apply src.
|
unfold expr_neg in src; rewrite exprRel in src. apply src.
|
||||||
congruence.
|
congruence.
|
||||||
+ elimtype False.
|
+ elimtype False.
|
||||||
unfold expr_neg in src; rewrite exprRel in src. apply src.
|
unfold expr_neg in src; rewrite exprRel in src. apply src.
|
||||||
congruence.
|
congruence.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Lemma Sn_noerror_n_noerror (n: nat) (s: Instr) (sMem: Mem) (m: Mem):
|
Lemma Sn_noerror_n_noerror (n: nat) (s: Instr) (sMem: Mem) (m: Mem):
|
||||||
interp (nth_iterate s (S n)) (MemElem sMem) = MemElem m
|
interp (nth_iterate s (S n)) (MemElem sMem) = MemElem m
|
||||||
-> exists m0, interp (nth_iterate s n) (MemElem sMem) = MemElem m0
|
-> exists m0, interp (nth_iterate s n) (MemElem sMem) = MemElem m0
|
||||||
/\ interp s (MemElem m0) = MemElem m.
|
/\ interp s (MemElem m0) = MemElem m.
|
||||||
Proof.
|
Proof.
|
||||||
intro HSn.
|
intro HSn.
|
||||||
destruct (interp (nth_iterate s n) (MemElem sMem)) eqn:nRel.
|
destruct (interp (nth_iterate s n) (MemElem sMem)) eqn:nRel.
|
||||||
- rewrite (unfold_one_iter s sMem n) in HSn.
|
- rewrite (unfold_one_iter s sMem n) in HSn.
|
||||||
rewrite nRel in HSn. apply error_leads_to_no_success in HSn.
|
rewrite nRel in HSn. apply error_leads_to_no_success in HSn.
|
||||||
elimtype False. apply HSn.
|
elimtype False. apply HSn.
|
||||||
- exists m0; unfold MemElem. split.
|
- exists m0; unfold MemElem. split.
|
||||||
* trivial.
|
* trivial.
|
||||||
* rewrite <- nRel; simpl. apply HSn.
|
* rewrite <- nRel; simpl. apply HSn.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Lemma greater_n_noerror (n1 n2: nat) (s: Instr) (sMem: Mem) (m: Mem):
|
Lemma greater_n_noerror (n1 n2: nat) (s: Instr) (sMem: Mem) (m: Mem):
|
||||||
n1 < n2
|
n1 < n2
|
||||||
-> interp (nth_iterate s n2) (MemElem sMem) = MemElem m
|
-> interp (nth_iterate s n2) (MemElem sMem) = MemElem m
|
||||||
-> exists m0, interp (nth_iterate s n1) (MemElem sMem) = MemElem m0.
|
-> exists m0, interp (nth_iterate s n1) (MemElem sMem) = MemElem m0.
|
||||||
Proof.
|
Proof.
|
||||||
intros nRel eventuallySound.
|
intros nRel eventuallySound.
|
||||||
assert (forall nDecr, nDecr <= n2 - n1 ->
|
assert (forall nDecr, nDecr <= n2 - n1 ->
|
||||||
exists m0,
|
exists m0,
|
||||||
interp (nth_iterate s (n2 - nDecr)) (MemElem sMem) = MemElem m0).
|
interp (nth_iterate s (n2 - nDecr)) (MemElem sMem) = MemElem m0).
|
||||||
* intros mDecr mDecrRel. induction mDecr.
|
* intros mDecr mDecrRel. induction mDecr.
|
||||||
+ exists m.
|
+ exists m.
|
||||||
assert (n2 = n2 - 0).
|
assert (n2 = n2 - 0).
|
||||||
{ unfold Nat.sub. destruct n2; trivial. }
|
{ unfold Nat.sub. destruct n2; trivial. }
|
||||||
{ rewrite <- H. assumption. }
|
{ rewrite <- H. assumption. }
|
||||||
+ assert (mDecr <= n2 - n1).
|
+ assert (mDecr <= n2 - n1).
|
||||||
{ omega. }
|
{ omega. }
|
||||||
{ elim (IHmDecr H). intros memNext memNextRel.
|
{ elim (IHmDecr H). intros memNext memNextRel.
|
||||||
elim (Sn_noerror_n_noerror (n2 - (S mDecr)) s sMem memNext).
|
elim (Sn_noerror_n_noerror (n2 - (S mDecr)) s sMem memNext).
|
||||||
intros memNow [memNowRel memNowInterp].
|
intros memNow [memNowRel memNowInterp].
|
||||||
exists memNow. apply memNowRel.
|
exists memNow. apply memNowRel.
|
||||||
assert (S (n2 - S mDecr) = n2 - mDecr). omega.
|
assert (S (n2 - S mDecr) = n2 - mDecr). omega.
|
||||||
rewrite H0. apply memNextRel.
|
rewrite H0. apply memNextRel.
|
||||||
}
|
}
|
||||||
* assert (n2 - n1 <= n2 - n1). omega. elim (H (n2 - n1) H0).
|
* assert (n2 - n1 <= n2 - n1). omega. elim (H (n2 - n1) H0).
|
||||||
intros memRes memResRel. exists memRes.
|
intros memRes memResRel. exists memRes.
|
||||||
assert (n2 - (n2 - n1) = n1). omega. rewrite H1 in memResRel.
|
assert (n2 - (n2 - n1) = n1). omega. rewrite H1 in memResRel.
|
||||||
assumption.
|
assumption.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Lemma unwrap_CpoElem (T: Type) :
|
Lemma unwrap_CpoElem (T: Type) :
|
||||||
forall m1 m2, CpoElem T m1 = CpoElem T m2 -> m1 = m2.
|
forall m1 m2, CpoElem T m1 = CpoElem T m2 -> m1 = m2.
|
||||||
Proof.
|
Proof.
|
||||||
intros m1 m2 cpoEq. congruence.
|
intros m1 m2 cpoEq. congruence.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Theorem hoare_provability_implies_consequence :
|
Theorem hoare_provability_implies_consequence :
|
||||||
forall (pre: Assert), forall (s: Instr), forall (post: Assert),
|
forall (pre: Assert), forall (s: Instr), forall (post: Assert),
|
||||||
( |- [| pre |] s [| post |] ) % assert
|
( |- [| pre |] s [| post |] ) % assert
|
||||||
-> ( |= [| pre |] s [| post |] ) % assert.
|
-> ( |= [| pre |] s [| post |] ) % assert.
|
||||||
Proof.
|
Proof.
|
||||||
intros pre instr post. intros deduction.
|
intros pre instr post. intros deduction.
|
||||||
induction deduction; intros mem preInMem.
|
induction deduction; intros mem preInMem.
|
||||||
- exact preInMem.
|
- exact preInMem.
|
||||||
- simpl; trivial.
|
- simpl; trivial.
|
||||||
- exact preInMem.
|
- exact preInMem.
|
||||||
- apply (weaken_in_conseq post' post (interp s (MemElem mem)) H0).
|
- apply (weaken_in_conseq post' post (interp s (MemElem mem)) H0).
|
||||||
apply IHdeduction. apply H. exact preInMem.
|
apply IHdeduction. apply H. exact preInMem.
|
||||||
- simpl; destruct (interp s1 (MemElem mem)) eqn:mRel.
|
- simpl; destruct (interp s1 (MemElem mem)) eqn:mRel.
|
||||||
* fold MemError. rewrite (interp_of_error s2); simpl; trivial.
|
* fold MemError. rewrite (interp_of_error s2); simpl; trivial.
|
||||||
* apply (IHdeduction2 m). unfold hoare_consequence in IHdeduction1.
|
* apply (IHdeduction2 m). unfold hoare_consequence in IHdeduction1.
|
||||||
specialize IHdeduction1 with mem as IH1_mem.
|
specialize IHdeduction1 with mem as IH1_mem.
|
||||||
rewrite mRel in IH1_mem. apply IH1_mem. assumption.
|
rewrite mRel in IH1_mem. apply IH1_mem. assumption.
|
||||||
- simpl; destruct (expr mem =? 0)%Z eqn:branchEqn.
|
- simpl; destruct (expr mem =? 0)%Z eqn:branchEqn.
|
||||||
* apply (IHdeduction2 mem). unfold assertOfExpr.
|
* apply (IHdeduction2 mem). unfold assertOfExpr.
|
||||||
unfold assertAnd. split.
|
unfold assertAnd. split.
|
||||||
+ assumption.
|
+ assumption.
|
||||||
+ unfold assertNot. rewrite <- Z.eqb_eq. congruence.
|
+ unfold assertNot. rewrite <- Z.eqb_eq. congruence.
|
||||||
* apply (IHdeduction1 mem). unfold assertOfExpr.
|
* apply (IHdeduction1 mem). unfold assertOfExpr.
|
||||||
unfold assertAnd. split.
|
unfold assertAnd. split.
|
||||||
+ assumption.
|
+ assumption.
|
||||||
+ rewrite <- Z.eqb_eq. congruence.
|
+ rewrite <- Z.eqb_eq. congruence.
|
||||||
- unfold conseq_or_bottom.
|
- unfold conseq_or_bottom.
|
||||||
destruct (interp (while expr sBody) (MemElem mem)) eqn:interpRel.
|
destruct (interp (while expr sBody) (MemElem mem)) eqn:interpRel.
|
||||||
* trivial.
|
* trivial.
|
||||||
* elim (certain_termination sBody expr (MemElem mem)).
|
* elim (certain_termination sBody expr (MemElem mem)).
|
||||||
intros n [lastIter [notLastIter isWhile] ].
|
intros n [lastIter [notLastIter isWhile] ].
|
||||||
rewrite isWhile in interpRel.
|
rewrite isWhile in interpRel.
|
||||||
destruct n.
|
destruct n.
|
||||||
{ simpl in lastIter. simpl in interpRel; unfold MemElem in interpRel.
|
{
|
||||||
unfold assertAnd. apply (unwrap_CpoElem Mem) in interpRel. split.
|
simpl in lastIter. simpl in interpRel; unfold MemElem in interpRel.
|
||||||
{ rewrite interpRel in preInMem; assumption. }
|
unfold assertAnd. apply (unwrap_CpoElem Mem) in interpRel. split.
|
||||||
{ apply expr_neg_consistency; rewrite <- interpRel; assumption. }
|
{ rewrite interpRel in preInMem; assumption. }
|
||||||
}
|
{ apply expr_neg_consistency; rewrite <- interpRel; assumption. }
|
||||||
unfold assertAnd; split.
|
}
|
||||||
+ apply conseq_or_bottom_is_conseq. unfold MemElem.
|
unfold assertAnd; split.
|
||||||
rewrite <- interpRel.
|
+ apply conseq_or_bottom_is_conseq. unfold MemElem.
|
||||||
assert (forall n1, n1 <= (S n) ->
|
rewrite <- interpRel.
|
||||||
conseq_or_bottom inv
|
assert (forall n1, n1 <= (S n) ->
|
||||||
(interp (nth_iterate sBody n1) (MemElem mem))).
|
conseq_or_bottom inv
|
||||||
{ induction n1.
|
(interp (nth_iterate sBody n1) (MemElem mem))).
|
||||||
{ intros obvious. simpl. assumption. }
|
{ induction n1.
|
||||||
{ intros order; simpl.
|
{ intros obvious. simpl. assumption. }
|
||||||
unfold hoare_consequence in IHdeduction.
|
{ intros order; simpl.
|
||||||
assert (n1 < S n) as nOrder. omega.
|
unfold hoare_consequence in IHdeduction.
|
||||||
elim (greater_n_noerror n1 (S n) sBody mem m nOrder interpRel).
|
assert (n1 < S n) as nOrder. omega.
|
||||||
intros memN relMemN.
|
elim (greater_n_noerror n1 (S n) sBody mem m nOrder interpRel).
|
||||||
specialize (IHdeduction memN) as IHmem.
|
intros memN relMemN.
|
||||||
rewrite relMemN.
|
specialize (IHdeduction memN) as IHmem.
|
||||||
apply IHmem.
|
rewrite relMemN.
|
||||||
unfold assertAnd; split.
|
apply IHmem.
|
||||||
{ rewrite relMemN in IHn1; unfold MemElem in IHn1.
|
unfold assertAnd; split.
|
||||||
apply IHn1. omega.
|
{ rewrite relMemN in IHn1; unfold MemElem in IHn1.
|
||||||
}
|
apply IHn1. omega.
|
||||||
{ unfold assertOfExpr.
|
}
|
||||||
specialize (notLastIter n1).
|
{ unfold assertOfExpr.
|
||||||
rewrite relMemN in notLastIter.
|
specialize (notLastIter n1).
|
||||||
unfold satisfies_expr in notLastIter; simpl in notLastIter.
|
rewrite relMemN in notLastIter.
|
||||||
apply notLastIter. assumption.
|
unfold satisfies_expr in notLastIter; simpl in notLastIter.
|
||||||
}
|
apply notLastIter. assumption.
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
{
|
}
|
||||||
apply H. omega.
|
{
|
||||||
}
|
apply H. omega.
|
||||||
+ unfold assertNot; unfold assertOfExpr. rewrite interpRel in lastIter.
|
}
|
||||||
unfold satisfies_expr in lastIter.
|
+ unfold assertNot; unfold assertOfExpr. rewrite interpRel in lastIter.
|
||||||
unfold expr_neg in lastIter.
|
unfold satisfies_expr in lastIter.
|
||||||
destruct (expr m); simpl; congruence.
|
unfold expr_neg in lastIter.
|
||||||
+ rewrite interpRel; unfold MemError; congruence.
|
destruct (expr m); simpl; congruence.
|
||||||
|
+ rewrite interpRel; unfold MemError; congruence.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
(***** Weakest precondition **************************************************)
|
(***** Weakest precondition **************************************************)
|
||||||
|
|
||||||
Fixpoint wp (instr: Instr) (cond: Assert) : Assert := match instr with
|
Fixpoint wp (instr: Instr) (cond: Assert) : Assert := match instr with
|
||||||
| skip =>
|
| skip =>
|
||||||
cond
|
cond
|
||||||
| abort =>
|
| abort =>
|
||||||
assertTop
|
assertTop
|
||||||
| assign x expr =>
|
| assign x expr =>
|
||||||
cond [[ x <- expr expr ]]
|
cond [[ x <- expr expr ]]
|
||||||
| seq s1 s2 =>
|
| seq s1 s2 =>
|
||||||
wp s1 (wp s2 cond)
|
wp s1 (wp s2 cond)
|
||||||
| ifelse guard sIf sElse =>
|
| ifelse guard sIf sElse =>
|
||||||
(assertOfExpr guard -> wp sIf cond
|
(assertOfExpr guard -> wp sIf cond
|
||||||
/\ (~ (assertOfExpr guard) -> wp sElse cond)) % assert
|
/\ (~ (assertOfExpr guard) -> wp sElse cond)) % assert
|
||||||
| while guard body => assertTop
|
| while guard body => assertTop
|
||||||
end.
|
end.
|
||||||
|
|
||||||
Theorem wp_correctness (instr: Instr) (post: Assert) :
|
Theorem wp_correctness (instr: Instr) (post: Assert) :
|
||||||
( |= [| wp instr post |] instr [| post |] ) % assert.
|
( |= [| wp instr post |] instr [| post |] ) % assert.
|
||||||
Proof.
|
Proof.
|
||||||
(* TODO *)
|
|
||||||
Admitted.
|
Admitted.
|
||||||
|
|
||||||
|
(* vim: ts=2 sw=2
|
||||||
|
*)
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue