Commit 36b02cdc authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Cleanup.

parent ea6e4c53
......@@ -42,27 +42,6 @@ Parameter bounded_length:
(* -------------------------------------------------------------------------- *)
(* [Array.make]. *)
(* In practice, the parameter [n] of [Array.make] must not exceed the constant
[Sys.max_array_length]. In the specification, we ignore this aspect, as it
would pollute the client quite severely, without a clear benefit. If someday
we decide to make this precondition explicit, then we should guarantee that
[Sys.max_array_length] is at least [2^22 - 1], as this will help prove that
it is safe to allocate arrays of known small size. *)
Parameter make_spec :
curried 2%nat Array_ml.make /\
forall A n (x:A),
n >= 0 ->
app Array_ml.make [n x]
PRE \[]
POST (fun t => Hexists xs, t ~> Array xs \* \[xs = make n x]).
Hint Extern 1 (RegisterSpec Array_ml.make) => Provide make_spec.
(* -------------------------------------------------------------------------- *)
(* [Array.length]. *)
Parameter length_spec :
......@@ -104,6 +83,27 @@ Hint Extern 1 (RegisterSpec Array_ml.set) => Provide set_spec.
(* -------------------------------------------------------------------------- *)
(* [Array.make]. *)
(* In practice, the parameter [n] of [Array.make] must not exceed the constant
[Sys.max_array_length]. In the specification, we ignore this aspect, as it
would pollute the client quite severely, without a clear benefit. If someday
we decide to make this precondition explicit, then we should guarantee that
[Sys.max_array_length] is at least [2^22 - 1], as this will help prove that
it is safe to allocate arrays of known small size. *)
Parameter make_spec :
curried 2%nat Array_ml.make /\
forall A n (x:A),
n >= 0 ->
app Array_ml.make [n x]
PRE \[]
POST (fun t => Hexists xs, t ~> Array xs \* \[xs = make n x]).
Hint Extern 1 (RegisterSpec Array_ml.make) => Provide make_spec.
(* -------------------------------------------------------------------------- *)
(* [Array.copy]. *)
Parameter copy_spec:
......@@ -193,42 +193,4 @@ Hint Extern 1 (RegisterSpec Array_ml.sub) => Provide sub_spec.
(* TEMPORARY todo: define [LibListZ.sub] at the logical level *)
(************************************************************)
(************************************************************)
(************************************************************)
(** FUTURE
(** The model of an imperative array is a sequence, represented as a list *)
Definition array (A:Type) := list A.
Parameter ArrayOf : forall a A (T:htype A a) (M:array A) (l:loc), hprop.
Notation "'Array'" := (ArrayOf Id).
Require Import LibBag.
(* -- with credits ---*)
Set Implicit Arguments.
Require Export LibInt LibListZ CFSpec CFPrint CFPrimSpec.
Generalizable Variables a A.
Parameter array_make_cst : nat.
Parameter ml_array_make_spec_direct : forall a,
Spec ml_array_make (n:int) (v:a) |R>>
R (\$ (abs n * array_make_cst))
(fun l => l ~> Array (make n v)).
Parameter ml_array_make_spec : forall a,
Spec ml_array_make (n:int) (v:a) |R>>
n >= 0 ->
R (\$ (abs n * array_make_cst))
(fun l => Hexists M, l ~> Array M \* \[M = make n v]).
Hint Extern 1 (RegisterSpecCredits ml_array_make) => Provide ml_array_make_spec.
*)
(* TODO: spec of arrays with credits *)
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