Compare commits
2 commits
d1b62ad2b5
...
93336c705e
Author | SHA1 | Date | |
---|---|---|---|
Théophile Bastian | 93336c705e | ||
Théophile Bastian | 06f655c1c1 |
96
wp.v
96
wp.v
|
@ -157,47 +157,45 @@ Notation "a [[ x <- 'expr' z ]]" := (substAssertExpr a x z)
|
||||||
Definition assertOfExpr : Expr -> Assert :=
|
Definition assertOfExpr : Expr -> Assert :=
|
||||||
fun expr mem => expr mem <> 0%Z.
|
fun expr mem => expr mem <> 0%Z.
|
||||||
|
|
||||||
Definition assertImplLogical : Assert -> Assert -> Prop :=
|
Definition assertImplLogical (a1 a2: Assert): Prop :=
|
||||||
fun a1 a2 => forall (m : Mem), (a1 m) -> (a2 m).
|
forall (m: Mem), (a1 m) -> (a2 m).
|
||||||
|
|
||||||
|
|
||||||
(***** Hoare provability *****************************************************)
|
(***** Hoare provability *****************************************************)
|
||||||
|
|
||||||
Parameter hoare_provability : Assert -> Instr -> Assert -> Prop.
|
Reserved Notation "|- [| x |] y [| z |]" (at level 30).
|
||||||
Notation "|- [| pre |] instr [| post |]" :=
|
|
||||||
(hoare_provability pre instr post) (at level 30): assert.
|
|
||||||
|
|
||||||
Axiom h_skip: forall (asser: Assert), ( |- [|asser|] skip [|asser|]) % assert.
|
Inductive hoare_provability : Assert -> Instr -> Assert -> Prop :=
|
||||||
Axiom h_abort: forall (a1:Assert), forall (a2: Assert),
|
| H_skip: forall pre, hoare_provability pre skip pre
|
||||||
(|- [|a1|] abort [|a2|]) % assert.
|
| H_abort: forall pre, forall post, hoare_provability pre abort post
|
||||||
Axiom h_assign: forall (asser: Assert), forall (x: Var), forall (e: Expr),
|
| H_assign: forall post, forall (x: Var), forall (e: Expr),
|
||||||
(|- [| asser [[ x <- expr e ]] |] (assign x e) [|asser|]) % assert.
|
(|- [| post [[ x <- expr e ]] |] (assign x e) [| post |]) % assert
|
||||||
Axiom h_conseq:
|
| H_conseq:
|
||||||
forall (a1: Assert), forall (a1': Assert),
|
forall pre, forall post,
|
||||||
forall (a2: Assert), forall (a2': Assert),
|
forall pre', forall post',
|
||||||
forall (s: Instr),
|
forall s,
|
||||||
(|- [| a1' |] s [| a2' |]) % assert ->
|
|
||||||
(assertImplLogical a1 a1') ->
|
(|- [| pre' |] s [| post' |]) % assert ->
|
||||||
(assertImplLogical a2' a2) ->
|
(assertImplLogical pre pre') ->
|
||||||
(|- [| a1 |] s [| a2 |]) % assert.
|
(assertImplLogical post' post) ->
|
||||||
Axiom h_seq:
|
(|- [| pre |] s [| post |]) % assert
|
||||||
forall (a1: Assert), forall (a2: Assert), forall (a3: Assert),
|
| H_seq:
|
||||||
forall (s1: Instr), forall (s2: Instr),
|
forall pre, forall mid, forall post, forall s1, forall s2,
|
||||||
(|- [|a1|] s1 [|a2|]) % assert -> (|- [|a2|] s2 [|a3|]) % assert ->
|
(|- [|pre|] s1 [|mid|]) % assert ->
|
||||||
(|- [|a1|] (seq s1 s2) [|a3|]) % assert.
|
(|- [|mid|] s2 [|post|]) % assert ->
|
||||||
Axiom h_if:
|
(|- [|pre|] (seq s1 s2) [|post|]) % assert
|
||||||
forall (a1: Assert), forall (a2: Assert),
|
| H_if:
|
||||||
forall (e: Expr),
|
forall pre, forall post, forall expr, forall sIf, forall sElse,
|
||||||
forall (s1: Instr), forall (s2: Instr),
|
(|- [| pre /\ (assertOfExpr expr) |] sIf [| post |]) % assert ->
|
||||||
(|- [| a1 /\ (assertOfExpr e) |] s1 [| a2 |]) % assert ->
|
(|- [| pre /\ ~(assertOfExpr expr) |] sElse [| post |]) % assert ->
|
||||||
(|- [| a1 /\ ~ (assertOfExpr e) |] s2 [| a2 |]) % assert ->
|
(|- [| pre |] (ifelse expr sIf sElse) [| post |]) % assert
|
||||||
(|- [| a1 |] (ifelse e s1 s2) [| a2 |]) % assert.
|
| H_while:
|
||||||
Axiom h_while:
|
forall inv, forall expr, forall sBody,
|
||||||
forall (inv: Assert),
|
(|- [| inv /\ (assertOfExpr expr) |] sBody [| inv |]) % assert ->
|
||||||
forall (e: Expr),
|
(|- [| inv |] (while expr sBody)
|
||||||
forall (s: Instr),
|
[| inv /\ ~ (assertOfExpr expr) |]) % assert
|
||||||
(|- [| inv /\ (assertOfExpr e) |] s [| inv |]) % assert ->
|
where "|- [| pre |] instr [| post |]" :=
|
||||||
(|- [| inv |] (while e s) [| inv /\ ~ (assertOfExpr e) |]) % assert.
|
(hoare_provability pre instr post) : assert.
|
||||||
|
|
||||||
(***** Hoare: provability implies consequence ********************************)
|
(***** Hoare: provability implies consequence ********************************)
|
||||||
|
|
||||||
|
@ -214,10 +212,32 @@ Definition hoare_consequence (pre: Assert) (instr: Instr) (post: Assert) :=
|
||||||
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:
|
||||||
|
forall a1, forall a2, forall m,
|
||||||
|
assertImplLogical a1 a2 -> conseq_or_bottom a1 m ->
|
||||||
|
conseq_or_bottom a2 m.
|
||||||
|
Proof.
|
||||||
|
intros a1 a2 m impl conseq. destruct m.
|
||||||
|
- apply conseq.
|
||||||
|
- simpl. unfold assertImplLogical in impl. apply (impl m). apply conseq.
|
||||||
|
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.
|
||||||
(* TODO *)
|
intros pre instr post. intros deduction.
|
||||||
Admitted.
|
induction deduction; intros mem preInMem; simpl.
|
||||||
|
- exact preInMem.
|
||||||
|
- trivial.
|
||||||
|
- exact preInMem.
|
||||||
|
- apply (weaken_in_conseq post' post (interp s (MemElem mem)) H0).
|
||||||
|
apply IHdeduction. apply H. exact preInMem.
|
||||||
|
- destruct (interp s1 (MemElem mem)) eqn:mRel.
|
||||||
|
admit.
|
||||||
|
apply (IHdeduction2 m). unfold hoare_consequence in IHdeduction1.
|
||||||
|
specialize IHdeduction1 with mem as IH1_mem.
|
||||||
|
rewrite mRel in IH1_mem. apply IH1_mem. assumption.
|
||||||
|
-
|
||||||
|
|
Loading…
Reference in a new issue