Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

Commit 09fdfa70 authored by charguer's avatar charguer
Browse files

mutable_queue_part1

parent 37f38437
......@@ -44,7 +44,7 @@ Proof.
{ xret. xsimpl. rewrite I1. rewrite I2. auto. auto. }
{ xret. xsimpl. rewrite I1. applys app_not_empty_l.
intros E. subst. false* C. } }
(* Shorter proof *)
(* Shorter proof *)
{ xmatch; xrets.
{ rewrite* I2 in I1. }
{ subst L. applys* app_not_empty_l. intros ->. false* C . } }
......@@ -79,7 +79,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 r] x [I1 I2]. xcf. xmatch. xapp.
xpull. intros I'. xsimpl. rewrite I1.
rew_list in *. auto.
Qed.
......
module StackList = struct
type 'a t = {
mutable front : 'a list;
mutable back : 'a list;
mutable size : int }
let create () =
{ front = [];
back = [];
size = 0 }
let length s =
s.size
let is_empty s =
s.size = 0
let push x s =
s.back <- x :: s.back;
s.size <- s.size + 1
let pop s =
if s.front = [] then begin
s.front <- s.back;
s.back <- [];
end;
match s.front with
| [] -> raise Not_found
| x::f ->
s.front <- f;
s.size <- s.size - 1;
x
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
type 'a t
val create : unit -> 'a t
val length : 'a t -> int
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 MutableQueue_ml.
Require Import TLC.LibListZ.
Implicit Types n : int.
Implicit Types q : loc.
(* TODO: update TLC *)
Lemma length_zero_eq_eq_nil : forall A (l:list A),
(LibListZ.length l = 0) = (l = nil).
Proof using.
intros. unfolds length. rewrite <-LibList.length_zero_eq_eq_nil. math.
Qed.
(*******************************************************************)
(** Representation Predicate *)
Definition Queue A (L:list A) q :=
Hexists (f:list A) (b:list A) (n:int),
q ~> `{ front' := f; back' := b; size' := n }
\* \[ L = f ++ rev b ] \* \[ n = length L ].
(*******************************************************************)
(** Unfolding and folding of the representation predicate *)
Lemma Queue_open : forall A (L:list A) f r,
(f,r) ~> Queue L ==>
\[L = f ++ rev r /\ (f = nil -> r = nil)].
Lemma Queue_open : forall q A (L:list A),
q ~> Queue L ==>
Hexists f b n, q ~> `{ front' := f; back' := b; size' := n }
\* \[ L = f ++ rev b ] \* \[ n = length L ].
Proof using.
dup 2.
{ intros. xunfold Queue. hpull. intros. hcancel. auto.
(* Try [hcancel 3] to see how it works *) }
{ intros. xunfolds~ Queue. }
intros. xunfolds* Queue.
Qed.
Lemma Queue_close : forall A f r,
(f = nil -> r = nil) ->
\[] ==> (f,r) ~> Queue (f ++ rev r).
Proof using. intros. xunfolds~ Stack. Qed.
Lemma Queue_close : forall q A (f b:list A) n,
n = length (f ++ rev b) ->
q ~> `{ front' := f; back' := b; size' := n } ==>
q ~> Queue (f ++ rev b).
Proof using. intros. xunfolds* Queue. Qed.
Arguments Queue_close : clear implicits.
......@@ -29,96 +51,69 @@ Arguments Queue_close : clear implicits.
[Queue], excluding the pointer. (Here, we have one underscore for [L].) *)
Hint Extern 1 (RegisterOpen (Queue _)) =>
Provide Stack_open.
Provide Queue_open.
Hint Extern 1 (RegisterClose (record_repr _)) =>
Provide Stack_close.
Provide Queue_close.
--------------
(** Definition of [r ~> Stack L], which is a notation for [Stack L r] of type [hprop] *)
Definition Queue A (L:list A) r :=
Hexists n,
r ~> `{ items' := L; size' := n }
\* \[ n = length L ].
(** Verification of the code *)
(*******************************************************************)
(** Create *)
Lemma create_spec : forall (A:Type),
app create [tt]
PRE \[]
POST (fun r => r ~> Stack (@nil A)).
POST (fun q => q ~> Queue (@nil A)).
Proof using.
xcf. dup 2.
{ xapp. intros r. (* or just [xapp. => r] *)
xclose r. auto. xsimpl. }
{ xapp ;=> r. xclose~ r. }
xcf. xapp ;=> r. xclose* r.
(* details: xcf. xapp. intros r. xclose r. auto. xsimpl. *)
Qed.
Lemma size_spec : forall (A:Type) (L:list A) (s:loc),
app size [s]
INV (s ~> Stack L)
Hint Extern 1 (RegisterSpec create) => Provide create_spec.
(*******************************************************************)
(** Length *)
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]).
(* Remark: the above is a notation for:
app size [s]
PRE (s ~> Stack L)
POST (fun n => \[n = length L] \* s ~> Stack L).
*)
(* Details:
app MutableQueue_ml.length [s]
PRE (s ~> Stack L)
POST (fun n => \[n = length L] \* s ~> Stack L). *)
Proof using.
xcf. (* TODO: add xopens to do xpull *)
xopen s. (* details: xchange (@Stack_open s). *)
xpull ;=> n Hn.
(* interesting: do [unfold tag] here, to unfold this identity
function used to decorate the file. *)
xapp. (* computes on-the-fly the record_get specification *)
intros m.
xpull ;=> ->. (* details: [xpull. intros E. subst E.] *)
xclose s. (* details: xchange (@Stack_close s). *)
auto. xsimpl. math.
(* Here we have an issue because Coq is a bit limited.
Workaround to discharge the remaining type: *)
Unshelve. solve_type. (* TODO: support [xcf A] in the beginning *)
xcf.
xopen q. (* details: xchange (@Stack_open s). *)
xpull ;=> f b n I1 I2.
xapp. xpull. intros ->.
xclose q. (* details: xchange (@Stack_close s). *)
{ subst*. }
xsimpl*.
(* Here we have an issue because Coq is unable to infer a type. *)
Unshelve. solve_type.
Qed.
Lemma length_zero_iff_nil : forall A (L:list A),
length L = 0 <-> L = nil.
Proof using.
intros. destruct L; rew_list. (* [rew_list] normalizes list expressions *)
{ autos*. (* [intuition eauto] *) }
{ iff M; false; math. (* [iff M] is [split; intros M] *) }
Qed.
Lemma is_empty_spec : forall (A:Type) (L:list A) (s:loc),
(* <EXO> *)
app is_empty [s]
INV (s ~> Stack L)
(*******************************************************************)
(** Length *)
Lemma is_empty_spec : forall A (L:list A) q,
app is_empty [q]
INV (q ~> Queue L)
POST (fun b => \[b = isTrue (L = nil)]).
(* </EXO> *)
Proof using.
(* Hint: use [xopen] then [xclose] like in [size_spec].
Also use [xcf], [xpull], [xapps], [xrets],
and lemma [length_zero_iff_nil] from above. *)
(* <EXO> *)
xcf.
(* Note that the boolean expression [n = 0] from Caml
was automatically translated into [isTrue (x0__ = 0)];
Indeed, [Ret_ P] is notation for [Ret (isTrue P)]. *)
xopen s. xpull ;=> n Hn. xapps. xclose~ s.
dup 2.
{ xret_no_clean.
reflect_clean tt. (* automatically called by [hsimpl] *)
hsimpl.
subst. apply length_zero_iff_nil. }
{ xrets. subst. apply length_zero_iff_nil. }
(* </EXO> *)
xcf. xopen q. xpull ;=> f b n I1 I2. xapps. xclose* q. xrets.
subst n. rewrite* length_zero_eq_eq_nil.
Unshelve. solve_type.
Qed.
(*
(*******************************************************************)
(** Push *)
Lemma push_spec : forall (A:Type) (L:list A) (s:loc) (x:A),
app push [x s]
PRE (s ~> Stack L)
......@@ -141,8 +136,9 @@ Qed.
Hint Extern 1 (RegisterSpec push) => Provide push_spec.
(* [xapp] on a call to push.
Otherwise, need to do [xapp_spec push_spec]. *)
(*******************************************************************)
(** Pop *)
Lemma pop_spec : forall (A:Type) (L:list A) (s:loc),
L <> nil ->
......@@ -157,5 +153,4 @@ Proof using.
(* </EXO> *)
Qed.
*)
\ No newline at end of file
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