Commit d4fdebf2 authored by charguer's avatar charguer
Browse files

tuto_stack

parent d7487085
......@@ -101,7 +101,7 @@ module StackList = struct
{ items = [];
size = 0 }
let length s =
let size s =
s.size
let is_empty s =
......@@ -153,7 +153,7 @@ module Vector = struct
size = size;
default = def; }
let length t =
let size t =
t.size
let get t i =
......
......@@ -10,15 +10,16 @@ Hint Resolve index_bounds_impl : maths.
Hint Resolve index_length_unfold int_index_prove : maths.
Hint Resolve index_update : maths.
(*
Hint Resolve length_nonneg : maths.
Hint Extern 1 (length (?l[?i:=?v]) = _) => rewrite length_update.
Hint Resolve length_make : maths.
Hint Extern 1 (length ?M = _) => subst M : maths.
Hint Constructors Forall.
Global Opaque Z.mul.
(* LATER
Hint Resolve length_nonneg : maths.
Hint Extern 1 (length (?l[?i:=?v]) = _) => rewrite length_update.
Hint Resolve length_make : maths.
Hint Extern 1 (length ?M = _) => subst M : maths.
Hint Constructors Forall.
Global Opaque Z.mul.
*)
(***********************************************************************)
(** Mathematical definitions *)
......@@ -423,6 +424,139 @@ Proof using.
Qed.
(***********************************************************************)
(** Stack *)
(*---------------------------------------------------------------------*)
(*----
module StackList = struct
type 'a t = {
mutable items : 'a list;
mutable size : int }
let create () =
{ items = [];
size = 0 }
let size s =
s.size
let is_empty s =
s.size = 0
let push x s =
s.items <- x :: s.items;
s.size <- s.size + 1
let pop s =
match s.items with
| hd::tl ->
s.items <- tl;
s.size <- s.size - 1;
hd
| [] -> assert false
end
----*)
Module StackListProof.
Import StackList_ml.
Definition Stack A (L:list A) r :=
Hexists n,
r ~> `{ items' := L; size' := n }
\* \[ n = length L ].
(**--- begin customization of [xopen] and [xclose] for [Stack] ---*)
Lemma Stack_open : forall r A (L:list A),
r ~> Stack L ==>
Hexists n, r ~> `{ items' := L; size' := n } \* \[ n = length L ].
Proof using. intros. xunfolds~ Stack. Qed.
Lemma Stack_close : forall r A (L:list A) (n:int),
n = length L ->
r ~> `{ items' := L; size' := n } ==>
r ~> Stack L.
Proof using. intros. xunfolds~ Stack. Qed.
Implicit Arguments Stack_close [].
Hint Extern 1 (RegisterOpen (Stack _)) =>
Provide Stack_open.
Hint Extern 1 (RegisterClose (record_repr _)) =>
Provide Stack_close.
(*--- end ---*)
Lemma create_spec : forall (A:Type),
app create [tt]
PRE \[]
POST (fun r => r ~> Stack (@nil A)).
Proof using.
xcf. xapps. => r. xclose r. auto. xsimpl.
Qed.
Lemma size_spec : forall (A:Type) (L:list A) (s:loc),
app size [s]
INV (s ~> Stack L)
POST (fun n => \[n = length L]).
Proof using.
xcf.
xopen s. xpull ;=> n Hn. xapp. => m. xpull ;=> E.
xclose s. auto. xsimpl~.
Unshelve. solve_type. (* todo: xcf A *)
Qed.
Lemma length_zero_iff_nil : forall A (L:list A),
length L = 0 <-> L = nil.
Proof using.
=>. subst. destruct L; rew_list. autos*. iff M; false; math.
Qed.
Lemma is_empty_spec : forall (A:Type) (L:list A) (s:loc),
(* <EXO> *)
app is_empty [s]
INV (s ~> Stack L)
POST (fun b => \[b = isTrue (L = nil)]).
(* </EXO> *)
Proof using.
(* <EXO> *)
xcf. xopen s. xpull ;=> n Hn. xapps. xclose~ s. xrets.
subst. apply length_zero_iff_nil.
(* </EXO> *)
Unshelve. solve_type. (* todo: xcf A *)
Qed.
Lemma push_spec : forall (A:Type) (L:list A) (s:loc) (x:A),
app push [x s]
PRE (s ~> Stack L)
POST (# s ~> Stack (x::L)).
Proof using.
(* <EXO> *)
xcf. xopen s. xpull ;=> n Hn. xapps. xapps. xapps. xapp.
xclose~ s. rew_list. math.
(* </EXO> *)
Qed.
Lemma pop_spec : forall (A:Type) (L:list A) (s:loc),
L <> nil ->
app pop [s]
PRE (s ~> Stack L)
POST (fun x => Hexists L', \[L = x::L'] \* s ~> Stack L').
Proof using.
(* <EXO> *)
=>> HL. xcf. xopen s. xpull ;=> n Hn. xapps. xmatch.
xapps. xapps. xapps. xret. xclose~ s. rew_list in Hn. math.
(* </EXO> *)
Qed.
(***********************************************************************)
(** Array *)
......
......@@ -281,9 +281,18 @@ Notation "F 'PRE' H 'POST' Q" :=
(tag tag_goal F H Q)
(at level 69, only parsing) : charac.
Notation "F 'PRE_KEEP' H 'POST' Q" :=
Notation "F 'PRE' H1 'INV' H2 'POST' Q" :=
(tag tag_goal F (H1 \* H2)%h (Q \*+ H2%h))
(at level 69,
format "'[v' F '/' '[' 'PRE' H1 ']' '/' '[' 'INV' H2 ']' '/' '[' 'POST' Q ']' ']'")
: charac.
Notation "F 'INV' H 'POST' Q" :=
(tag tag_goal F H%h (Q \*+ H%h))
(at level 69, only parsing) : charac.
(at level 69,
format "'[v' F '/' '[' 'INV' H ']' '/' '[' 'POST' Q ']' ']'")
: charac.
(********************************************************************)
......
......@@ -47,9 +47,9 @@ Parameter bounded_length:
Parameter length_spec :
curried 1%nat Array_ml.length /\
forall A (xs:list A) t,
app_keep Array_ml.length [t]
(t ~> Array xs)
(fun n => \[n = length xs]).
app Array_ml.length [t]
INV (t ~> Array xs)
POST (fun n => \[n = length xs]).
Hint Extern 1 (RegisterSpec Array_ml.length) => Provide length_spec.
......@@ -61,9 +61,9 @@ Parameter get_spec :
curried 2%nat Array_ml.get /\
forall A `{Inhab A} (xs:list A) t i,
index xs i ->
app_keep Array_ml.get [t i]
(t ~> Array xs)
\[= xs[i] ].
app Array_ml.get [t i]
INV (t ~> Array xs)
POST \[= xs[i] ].
Hint Extern 1 (RegisterSpec Array_ml.get) => Provide get_spec.
......@@ -109,9 +109,9 @@ Hint Extern 1 (RegisterSpec Array_ml.make) => Provide make_spec.
Parameter copy_spec:
curried 1%nat Array_ml.copy /\
forall A (xs:list A) t,
app_keep Array_ml.copy [t]
(t ~> Array xs)
(fun t' => t' ~> Array xs).
app Array_ml.copy [t]
INV (t ~> Array xs)
POST (fun t' => t' ~> Array xs).
Hint Extern 1 (RegisterSpec Array_ml.copy) => Provide copy_spec.
......@@ -186,12 +186,12 @@ Parameter sub_spec :
0 <= ofs ->
0 <= len ->
ofs + len <= length xs ->
app_keep Array_ml.sub [t ofs len]
(t ~> Array xs)
(fun t' => Hexists xs',
t' ~> Array xs' \*
\[length xs' = len] \*
\[forall i, ofs <= i < len -> xs'[i] = xs[i]]).
app Array_ml.sub [t ofs len]
INV (t ~> Array xs)
POST (fun t' => Hexists xs',
t' ~> Array xs'
\* \[length xs' = len]
\* \[forall i, ofs <= i < len -> xs'[i] = xs[i]]).
Hint Extern 1 (RegisterSpec Array_ml.sub) => Provide sub_spec.
......
......@@ -4,6 +4,8 @@ Require Import Pervasives_ml.
Generalizable Variable A.
(* TODO: add PRE/POST notation *)
(************************************************************)
(** Boolean *)
......@@ -259,11 +261,15 @@ Notation "r '~~>' v" := (hdata (Ref v) r)
(at level 32, no associativity) : heap_scope.
Lemma ref_spec : forall A (v:A),
app ref [v] \[] (fun r => r ~~> v).
app ref [v]
PRE \[]
POST (fun r => r ~~> v).
Proof using. xcf_go~. Qed.
Lemma infix_emark_spec : forall A (v:A) r,
app_keep infix_emark__ [r] (r ~~> v) \[= v].
app infix_emark__ [r]
INV (r ~~> v)
POST \[= v].
Proof using. xunfold @Ref. xcf_go~. Qed.
Lemma infix_colon_eq_spec : forall A (v w:A) r,
......@@ -283,11 +289,15 @@ Notation "'App'' r `:= x" := (App infix_colon_eq__ r x;)
format "'App'' r `:= x") : charac.
Lemma incr_spec : forall (n:int) r,
app incr [r] (r ~~> n) (# r ~~> (n+1)).
app incr [r]
PRE (r ~~> n)
POST (# r ~~> (n+1)).
Proof using. xcf_go~. Qed.
Lemma decr_spec : forall (n:int) r,
app decr [r] (r ~~> n) (# r ~~> (n-1)).
app decr [r]
PRE (r ~~> n)
POST (# r ~~> (n-1)).
Proof using. xcf_go~. Qed.
Hint Extern 1 (RegisterSpec incr) => Provide incr_spec.
......@@ -307,7 +317,7 @@ Axiom ref_spec_group : forall A (M:map loc A) (v:A),
Lemma infix_emark_spec_group : forall `{Inhab A} (M:map loc A) r,
r \indom M ->
app Pervasives_ml.infix_emark__ [r]
PRE_KEEP (Group Ref M)
INV (Group Ref M)
POST (fun x => \[x = M[r]]).
Proof using.
intros. rewrite~ (Group_rem r M). xapp. xsimpl~.
......@@ -328,11 +338,15 @@ Qed.
(** Pairs *)
Lemma fst_spec : forall A B (x:A) (y:B),
app fst [(x,y)] \[] \[= x].
app fst [(x,y)]
PRE \[]
POST \[= x].
Proof using. xcf_go~. Qed.
Lemma snd_spec : forall A B (x:A) (y:B),
app snd [(x,y)] \[] \[= y].
app snd [(x,y)]
PRE \[]
POST \[= y].
Proof using. xcf_go~. Qed.
Hint Extern 1 (RegisterSpec fst) => Provide fst_spec.
......@@ -343,7 +357,9 @@ Hint Extern 1 (RegisterSpec snd) => Provide snd_spec.
(** Unit *)
Lemma ignore_spec :
app ignore [tt] \[] \[= tt].
app ignore [tt]
PRE \[]
POST \[= tt].
Proof using. xcf_go~. Qed.
Hint Extern 1 (RegisterSpec ignore) => Provide ignore_spec.
......
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