Commit 0801f9a4 authored by charguer's avatar charguer
Browse files

infos

parent a3e2865c
......@@ -19,6 +19,9 @@ Definition Queue A (L:list A) (q:t_ A) : hprop :=
q ~> `{ front' := f; back' := b; size' := n }
\* \[ L = f ++ rev b /\ n = length L ].
(** Note: to reduce name clashes, field names are suffixed
with a quote symbol. *)
(** Note: [q] has type ['a t] is OCaml, translated as [t_ A]
in Coq. The type [t_ A] is defined as [loc], which is
the type of memory locations in CFML. *)
......@@ -43,7 +46,7 @@ Proof using. intros. xunfolds* Queue. Qed.
Arguments Queue_close : clear implicits.
(** Customization of [xopen] and [xclose] tactics for [Stack].
(** Customization of [xopen] and [xclose] tactics for [Queue].
These tactics avoid the need to call [hchange] or [xchange]
by providing explicitly the lemmas [Queue_open] and [Queue_close].
Note that the number of underscores avec [Queue] after the [RegisterOpen]
......@@ -64,8 +67,7 @@ Lemma create_spec : forall A,
PRE \[]
POST (fun q => q ~> Queue (@nil A)).
Proof using.
xcf. xapp ;=> r. xclose* r.
(* details: xcf. xapp. intros r. xclose r. auto. xsimpl. *)
xcf. xapp. intros r. xclose r. { auto. } { xsimpl. }
Qed.
Hint Extern 1 (RegisterSpec create) => Provide create_spec.
......@@ -75,19 +77,18 @@ Hint Extern 1 (RegisterSpec create) => Provide create_spec.
(** Length *)
Lemma length_spec : forall (A:Type) (L:list A) (q:loc),
(* app MutableQueue_ml.length [s]
PRE (q ~> Queue L)
POST (fun n => \[n = length L] \* q ~> Queue L).
*)
app MutableQueue_ml.length [q]
INV (q ~> Queue L)
POST (fun n => \[n = length L]).
(* Equivalent to:
app MutableQueue_ml.length [s]
PRE (s ~> Stack L)
POST (fun n => \[n = length L] \* s ~> Stack L). *)
Proof using.
xcf.
xopen q. (* details: xchange (@Stack_open s). *)
xpull ;=> f b n (I1&I2).
xapp. xpull. intros ->.
xclose q. { subst*. } (* details: xchange (@Stack_close s). *)
xopen q. xpull. intros f b n (I1&I2).
xapp. xpull. intros ->.
xclose q. { subst*. }
xsimpl*.
(* Here we have an issue because Coq is unable to infer a type. *)
Unshelve. solve_type.
......@@ -104,7 +105,8 @@ Lemma is_empty_spec : forall A (L:list A) q,
INV (q ~> Queue L)
POST (fun b => \[b = isTrue (L = nil)]).
Proof using.
xcf. xopen q. xpull ;=> f b n (I1&I2). xapps. xclose* q. xrets.
xcf. xopen q. xpull. intros f b n (I1&I2).
xapps. xclose* q. xrets.
subst n. rewrite lengthZ_zero_eq_eq_nil. tauto.
Unshelve. solve_type.
Qed.
......@@ -121,9 +123,9 @@ Lemma push_spec : forall A (L:list A) q x,
POST (fun (_:unit) => q ~> Queue (L ++ x::nil)).
Proof using.
xcf. xopen q. xpull. intros f b n (I1&I2).
xapps. xapp. xapps. xapp.
xclose q. { subst. rew_list. math. }
xsimpl. subst. rew_list*.
xapps. xapp. xapps. xapp. xclose q.
{ subst. rew_list. math. }
{ xsimpl. subst. rew_list*. }
Qed.
Hint Extern 1 (RegisterSpec push) => Provide push_spec.
......@@ -132,6 +134,22 @@ Hint Extern 1 (RegisterSpec push) => Provide push_spec.
(*******************************************************************)
(** Pop *)
(**
[[
let pop q =
if q.front = [] then begin
q.front <- List.rev q.back;
q.back <- [];
end;
match q.front with
| [] -> raise Not_found
| x::f ->
q.front <- f;
q.size <- q.size - 1;
x
]]
*)
Lemma pop_spec : forall A (L:list A) q,
L <> nil ->
app pop [q]
......@@ -142,12 +160,12 @@ Proof using.
xapps. xapps. xpolymorphic_eq.
xseq (fun (_:unit) => Hexists f' b',
q ~> `{ front' := f'; back' := b'; size' := n }
\* \[ L = f' ++ rev b' ] \* \[ f' = nil -> b' = nil ]).
\* \[ L = f' ++ rev b' ] \* \[ f' <> nil ]).
{ xif.
{ xapps. xrets. xapps. xapps. xsimpl. { auto. } { subst. rew_list*. } }
{ xrets. { intros. false. } { auto. } } }
{ xapps. xrets. xapps. xapps. xsimpl.
{ subst*. } { subst. rew_list*. } }
{ xrets*. } }
{ clears f b. intros f b I1 I3. xapps. xmatch.
{ xfail. rewrite I3 in I1. { rew_list in *. false. } { auto. } }
{ xapps. xapps. xapps. xret.
xclose q. { subst L. rew_list in *. math. }
xsimpl. subst L. rew_list*. } }
......@@ -167,7 +185,8 @@ Proof using.
xcf. xwhile; [|xok]. intros R LR HR. revert L2.
induction_wf IH: (@list_sub A) L1. hide IH.
intros. applys (rm HR).
xlet (fun b => \[b = isTrue (L1 <> nil)] \* q1 ~> Queue L1 \* q2 ~> Queue L2).
xlet (fun b => \[b = isTrue (L1 <> nil)]
\* q1 ~> Queue L1 \* q2 ~> Queue L2).
{ xapps. xrets. rew_isTrue*. }
intros ->. xif.
{ destruct L1 as [|x L1']; tryfalse.
......
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