Commit 2120a37b authored by POTTIER Francois's avatar POTTIER Francois

Trivial change: use PRE and POST notation.

parent f373f3b2
......@@ -28,8 +28,8 @@ Notation "'App'' t `[ i ] `<- x" := (App Array_ml.set t i x;)
(* The model of an imperative array is a sequence, represented as a list. *)
Parameter Array : forall A, list A -> loc -> hprop.
(* TODO: realize this definition as an iterated star of
the ownership of single cells, each of which being
(* TODO: realize this definition as an iterated star of
the ownership of single cells, each of which being
described using heap_is_single. *)
(* -------------------------------------------------------------------------- *)
......@@ -180,11 +180,13 @@ Lemma init_spec :
(forall (i : int) (xs : list A),
index n i ->
i = length xs ->
app f [i] (F xs) (fun x => F (xs & x))) ->
app f [i]
PRE (F xs)
POST (fun x => F (xs & x))) ->
app Array_ml.init [n f]
(F nil)
(fun t =>
Hexists xs, t ~> Array xs \* \[n = length xs] \* F xs).
PRE (F nil)
POST (fun t =>
Hexists xs, t ~> Array xs \* \[n = length xs] \* F xs).
Proof.
introv ? hf.
xcf.
......@@ -216,7 +218,7 @@ Proof.
{ rewrite app_nil_l. apply* singleton_prefix_make. }
}
(* 2. The loop body preserves the invariant. *)
{ clear x. intros i [ ? ? ]. xpull. intros xs zs. intros.
{ clear x. intros i [ ? ? ]. xpull; intros xs zs. intros.
xapp* hf as x.
xapp*.
xsimpl* (xs & x).
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment