Commit b3678430 authored by charguer's avatar charguer
Browse files

stackproof

parent ff3e381f
# /home/charguer/versions/coq-8.8.2/cfml/generator/makecmj.native -I /home/charguer/versions/coq-8.8.2/cfml/examples/Tour Stack.mli
# /home/charguer/versions/coq-8.8.2/cfml/generator/main.native -I /home/charguer/versions/coq-8.8.2/cfml/examples/Tour Stack.ml
# coqc -R /home/charguer/.opam/vocal_8.8.2/lib/coq/user-contrib/CFML/Stdlib CFML.Stdlib -R /home/charguer/versions/coq-8.8.2/cfml/examples/Tour EXAMPLE /home/charguer/versions/coq-8.8.2/cfml/examples/Tour/Stack_ml.
include ../Makefile.example
type elem = int
type node = { value : elem; sub : node Stack.t }
type contents = Empty | Nonempty of node
......
type 'a t = 'a list ref
let create () =
ref []
let is_empty s =
!s = []
let push x s =
s := x::!s
let pop s =
match !s with
| [] -> raise Not_found
| x::t -> s := t; x
type 'a t
val create : unit -> 'a t
val is_empty : 'a t -> bool
val push : 'a -> 'a t -> unit
val pop : 'a t -> 'a
Set Implicit Arguments.
Require Import CFML.CFLib.
Require Import Stdlib.
Require Import Stack_ml.
Require Import TLC.LibListZ.
Implicit Types n : int.
Implicit Types q : loc.
(*******************************************************************)
(** Representation Predicate *)
Definition Stack A (L:list A) (q:t_ A) :=
q ~~> L.
(*******************************************************************)
(** Unfolding and folding of the representation predicate *)
Lemma Stack_open : forall q A (L:list A),
q ~> Stack L ==> q ~~> L.
Proof using.
intros. xunfolds* Stack.
Qed.
Lemma Stack_close : forall q A (L:list A),
q ~~> L ==> q ~> Stack L.
Proof using. intros. xunfolds* Stack. Qed.
Arguments Stack_close : clear implicits.
(** Customization of [xopen] and [xclose] tactics for [Stack].
These tactics avoid the need to call [hchange] or [xchange]
by providing explicitly the lemmas [Stack_open] and [Stack_close].
Note that the number of underscores avec [Stack] after the [RegisterOpen]
needs to match the number of arguments of the representation predicate
[Stack], excluding the pointer. (Here, we have one underscore for [L].) *)
Hint Extern 1 (RegisterOpen (Stack _)) =>
Provide Stack_open.
Hint Extern 1 (RegisterClose (record_repr _)) =>
Provide Stack_close.
(*******************************************************************)
(** Create *)
Lemma create_spec : forall A,
app create [tt]
PRE \[]
POST (fun q => q ~> Stack (@nil A)).
Proof using.
xcf. xapp.
Qed.
Hint Extern 1 (RegisterSpec create) => Provide create_spec.
(*******************************************************************)
(** Is_empty *)
Lemma is_empty_spec : forall (A:Type) (L:list A) (q:loc),
app is_empty [q]
INV (q ~> Stack L)
POST (fun b => \[b = isTrue (L = nil)]).
Proof using.
xcf.
xopen q. (* details: xchange (@Stack_open s). *)
xapps. xapps. xpolymorphic_eq.
xsimpl*.
Qed.
Hint Extern 1 (RegisterSpec is_empty) => Provide is_empty_spec.
(*******************************************************************)
(** Push *)
Lemma push_spec : forall A (L:list A) q x,
app push [x q]
PRE (q ~> Stack L)
POST (fun (_:unit) => q ~> Stack (x::L)).
Proof using.
xcf. xopen q. xapps. xapps.
Qed.
Hint Extern 1 (RegisterSpec push) => Provide push_spec.
(*******************************************************************)
(** Pop *)
Lemma pop_spec : forall A (L:list A) q,
L <> nil ->
app pop [q]
PRE (q ~> Stack L)
POST (fun x => Hexists L', \[L = x::L'] \* q ~> Stack L').
Proof using.
introv N. xcf. xopen q. xapps. xmatch. xapps. xrets*.
Qed.
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