Commit 0225f8ed authored by charguer's avatar charguer
Browse files

renaming

parent fbe40b7d
(** Functional queue represented as a pair of lists:
- the front list stores elements in order of exit
- the back list stores elements in reverse order.
The structure maintains the front list nonempty
whenever possible. *)
(** Functional queue represented as a pair of lists.
The pair (front,back) represents the list [front ++ rev back].
The front list is maintained nonempty for nonempty queues. *)
type 'a queue = 'a list * 'a list
......
Set Implicit Arguments.
Require Import CFML.CFLib.
Require Import Stdlib.
Require Import CFML.CFLib Stdlib.
Require Import FunctionalQueue_ml.
(*******************************************************************)
(** Representation Predicate *)
Definition inv A (L:list A) (q:queue_ A) :=
let (f,r) := q in
(L = f ++ rev r)
/\ (f = nil -> r = nil).
Definition inv A (L:list A) (q:queue_ A) : Prop :=
let (f,b) := q in
(L = f ++ rev b)
/\ (f = nil -> b = nil).
(*******************************************************************)
......@@ -34,7 +33,7 @@ Lemma is_empty_spec : forall A (L:list A) q,
PRE \[]
POST (fun b => \[b = isTrue (L = nil)]).
Proof.
intros A L (f,r) [I1 I2]. xcf. dup.
intros A L (f,b) [I1 I2]. xcf. dup.
(* Detailed proof *)
{ xmatch.
{ xret. xsimpl. rewrite I1. rewrite I2. auto. auto. }
......@@ -52,14 +51,13 @@ Hint Extern 1 (RegisterSpec is_empty) => Provide is_empty_spec.
(*******************************************************************)
(** Check *)
Lemma check_spec : forall A (f r : list A),
app check [(f,r)]
Lemma check_spec : forall A (f b:list A),
app check [(f,b)]
PRE \[]
POST (fun q => \[inv (f ++ rev r) q]).
POST (fun q => \[inv (f ++ rev b) q]).
Proof.
xcf. xmatch.
{ (* xlet as f. xret. xpull. intros E. xret. xsimpl. unfolds. rew_list*. *)
xrets. xrets. unfolds. rew_list*. }
{ xrets. xrets. unfolds. rew_list*. }
{ xrets. split. { auto. } { intros ->. false* C. } }
Qed.
......@@ -75,7 +73,7 @@ Lemma push_spec : forall A (L:list A) q x,
PRE \[]
POST (fun q' => \[inv (L ++ x::nil) q']).
Proof.
intros A L [f r] x [I1 I2]. xcf. xmatch. xapp.
intros A L [f b] x [I1 I2]. xcf. xmatch. xapp.
xpull. intros I'. xsimpl. rewrite I1.
rew_list in *. auto.
Qed.
......@@ -93,7 +91,7 @@ Lemma pop_spec : forall A (L:list A) q,
PRE \[]
POST (fun '(x, q') => \[exists L', L = x::L' /\ inv L' q']).
Proof.
intros A L [f r] [I1 I2] N. xcf. xmatch.
intros A L [f b] [I1 I2] N. xcf. xmatch.
{ xfail. rewrite* I2 in I1. }
{ xapp. intros I'. xrets. rew_list in *. eauto. }
Qed.
......
......@@ -72,7 +72,7 @@ Lemma length_spec : forall (A:Type) (L:list A) (q:loc),
app MutableQueue_ml.length [q]
INV (q ~> Queue L)
POST (fun n => \[n = length L]).
(* Details:
(* Equivalent to:
app MutableQueue_ml.length [s]
PRE (s ~> Stack L)
POST (fun n => \[n = length L] \* s ~> Stack L). *)
......
(* Union-find: pointer-based implementation *)
(*
type contents = Root | Link of node
and node = contents ref
*)
type rank = int
type contents = Root of rank | Link of contents ref
......
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