Commit ea6e4c53 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Cleaned up [Array_proof].

parent 7fb4929c
Set Implicit Arguments.
Require Import CFLib.
Require Import Pervasives_ml Pervasives_proof.
Require Export LibListZ.
Require Import Array_ml.
Generalizable Variables A.
(************************************************************)
(** Builtin *)
Parameter Array : forall A (L:list A) (l:loc), hprop.
Parameter make_from_list_spec : curried 2%nat make_from_list /\
forall A (L:list A),
app make_from_list [L] \[] (fun t => t ~> Array L).
Hint Extern 1 (RegisterSpec make_from_list) => Provide make_from_list_spec.
Lemma make_empty_spec : forall A,
app make_empty [tt] \[] (fun l => l ~> Array (@nil A)).
Proof using.
xcf. xgo.
Qed.
Hint Extern 1 (RegisterSpec make_empty) => Provide make_empty_spec.
Parameter make_spec : curried 2%nat make /\
forall A (n:int) (v:A),
n >= 0 ->
app make [n v] \[] (fun t =>
Hexists L, t ~> Array L \* \[L = LibListZ.make n v]).
Hint Extern 1 (RegisterSpec make) => Provide make_spec.
Lemma make_spec_direct : forall A (n:int) (v:A),
n >= 0 ->
app make [n v] \[] (fun l => l ~> Array (LibListZ.make n v)).
Proof using.
intros. xapp~.
Qed.
Parameter length_spec : curried 1%nat length /\
forall A (L:list A) (t:loc),
app_keep length [t] (t ~> Array L) (fun n => \[n = LibListZ.length L]).
Hint Extern 1 (RegisterSpec length) => Provide length_spec.
Parameter get_spec : curried 2%nat get /\
forall `{Inhab A} (L:list A) (t:loc) (i:int),
index L i ->
app_keep get [t i] (t ~> Array L) \[= L[i] ].
Hint Extern 1 (RegisterSpec get) => Provide get_spec.
Parameter set_spec : curried 2%nat set /\
forall A (L:list A) (t:loc) (i:int) (v:A),
index L i ->
app set [t i v] (t ~> Array L) (# t ~> Array (L[i:=v])).
Hint Extern 1 (RegisterSpec set) => Provide set_spec.
(* NOTE: Check if correct *)
Parameter sub_spec : curried 3%nat sub /\
forall `{Inhab A} (L : list A) (a : loc) (ofs len : int),
0 <= ofs ->
ofs <= len ->
len <= LibListZ.length L ->
app_keep sub [a ofs len]
(a ~> Array L)
(fun a' => Hexists L',
a' ~> Array L' \*
\[LibListZ.length L' = len - ofs] \*
\[forall i, ofs <= i < len -> L'[i] = L[i]]).
Hint Extern 1 (RegisterSpec sub) => Provide sub_spec.
Notation "'App'' r `[ i ]" := (App get r i;)
(at level 69, r at level 0, no associativity,
format "'App'' r `[ i ]") : charac.
Notation "'App'' r `[ i ] `<- v" := (App set r i v;)
(at level 69, r at level 0, no associativity,
format "'App'' r `[ i ] `<- v") : charac.
(************************************************************)
(************************************************************)
(************************************************************)
(** 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.
*)
Require Import LibListZ.
Require Sys_ml.
Require Array_ml.
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* TODO: merge *)
(*
Set Implicit Arguments.
Require Import LibListZ LibMap LibInt.
Require Import CFSpec CFPrint CFPrim.
Require Array_ml.
Section Array.
(* Conventions. *)
Variable A : Type.
Implicit Types t : loc. (* array *)
Implicit Types i ofs len : int. (* index *)
(* -------------------------------------------------------------------------- *)
(* The model of an imperative array is a sequence, represented as a list. *)
(* An ad hoc notation for array accesses in OCaml code. For display only. *)
Parameter Array : list A -> loc -> hprop.
Notation "'App'' t `[ i ]" := (App Array_ml.get t i;)
(at level 69, t at level 0, no associativity,
format "'App'' t `[ i ]") : charac.
(* -------------------------------------------------------------------------- *)
Notation "'App'' t `[ i ] `<- x" := (App Array_ml.set t i x;)
(at level 69, t at level 0, no associativity,
format "'App'' t `[ i ] `<- x") : charac.
(* [Sys.max_array_length] is nonnegative. We do not guarantee anything more.
In reality, [Sys.max_array_length] is [2^22 - 1] on a 32-bit machine, and
[2^54 - 1] on a 64-bit machine. (10 bits are reserved in an array header,
the rest encodes the array length.) *)
(* -------------------------------------------------------------------------- *)
(* Ideally, we should guarantee that [Sys.max_array_length] is less than or
equal to [max_int]. This could be useful someday if we need to prove that
certain integer calculations cannot overflow. *)
(* The model of an imperative array is a sequence, represented as a list. *)
Parameter max_array_length_property:
0 <= ml_max_array_length.
Parameter Array : forall A, list A -> loc -> hprop.
(* -------------------------------------------------------------------------- *)
......@@ -170,9 +36,9 @@ Parameter max_array_length_property:
cannot overflow. *)
Parameter bounded_length:
forall l xs,
l ~> Array xs ==>
l ~> Array xs \* \[ length xs <= ml_max_array_length ].
forall A t (xs : list A),
t ~> Array xs ==>
t ~> Array xs \* \[ length xs <= Sys_ml.max_array_length ].
(* -------------------------------------------------------------------------- *)
......@@ -186,95 +52,183 @@ Parameter bounded_length:
it is safe to allocate arrays of known small size. *)
Parameter make_spec :
Spec Array_ml.make n v |R>>
n >= 0 ->
R \[] (fun l => Hexists xs, l ~> Array xs \* \[ xs = make n v ]).
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 :
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]).
Hint Extern 1 (RegisterSpec Array_ml.length) => Provide length_spec.
(* -------------------------------------------------------------------------- *)
(* [Array.get]. *)
Parameter get_spec :
Spec Array_ml.get l i |R>>
forall `{Inhab A} xs,
index xs i ->
keep R (l ~> Array xs) (fun x => \[ x = xs[i] ]).
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] ].
Hint Extern 1 (RegisterSpec Array_ml.get) => Provide get_spec.
(* -------------------------------------------------------------------------- *)
(* [Array.set]. *)
Parameter set_spec :
Spec Array_ml.set l i v |R>>
forall xs,
index xs i ->
R (l ~> Array xs) (# l ~> Array xs[i := v]).
curried 2%nat Array_ml.set /\
forall A (xs:list A) t i x,
index xs i ->
app Array_ml.set [t i x]
PRE ( t ~> Array xs)
POST (# t ~> Array (xs[i:=x])).
(* -------------------------------------------------------------------------- *)
(* [Array.length]. *)
Parameter length_spec :
Spec Array_ml.length l |R>>
forall xs,
keep R (l ~> Array xs) (fun n => \[ n = length xs ]).
Hint Extern 1 (RegisterSpec Array_ml.set) => Provide set_spec.
(* -------------------------------------------------------------------------- *)
(* [Array.copy]. *)
Parameter copy_spec:
Spec Array_ml.copy l |R>>
forall xs,
keep R (l ~> Array xs) (fun l' => l' ~> Array xs).
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).
Hint Extern 1 (RegisterSpec Array_ml.copy) => Provide copy_spec.
(* -------------------------------------------------------------------------- *)
(* [Array.fill]. *)
Parameter fill_spec :
Spec Array_ml.fill l ofs len x |R>>
forall `{Inhab A} xs,
0 <= ofs ->
ofs <= length xs ->
0 <= len ->
ofs + len <= length xs ->
R (l ~> Array xs) (# Hexists xs', l ~> Array xs' \*
curried 4%nat Array_ml.fill /\
forall A `{Inhab A} (xs:list A) t ofs len x,
0 <= ofs ->
ofs <= length xs ->
0 <= len ->
ofs + len <= length xs ->
app Array_ml.fill [t ofs len x]
PRE (t ~> Array xs)
POST (# Hexists xs', t ~> Array xs' \*
\[ length xs' = length xs ] \*
\[ forall i, ofs <= i < ofs + len -> xs'[i] = x ] \*
\[ forall i, (i < ofs \/ ofs + len <= i) -> xs'[i] = xs[i] ]
).
(* TEMPORARY todo: define [LibListZ.fill] at the logical level *)
(* -------------------------------------------------------------------------- *)
(* [Array.iter]. *)
Parameter iter_spec :
forall (I : list A -> hprop),
Spec Array_ml.iter f l |R>>
forall xs,
(forall x current,
prefix (current & x) xs ->
App f x; (I current) (# I (current & x))
) ->
R
(l ~> Array xs \* I nil)
(# l ~> Array xs \* I xs).
(* -------------------------------------------------------------------------- *)
curried 2%nat Array_ml.iter /\
forall A (I : list A -> hprop),
forall xs f t,
(
forall ys x,
prefix (ys & x) xs ->
app f [x]
PRE (I ys)
POST (# I (ys & x))
) ->
app Array_ml.iter [f t]
PRE ( t ~> Array xs \* I nil)
POST (# t ~> Array xs \* I xs ).
(* TEMPORARY iter: give a stronger spec with "read" access to array *)
(* TEMPORARY give a generic spec to iter-like functions *)
(* TEMPORARY missing fold_left *)
End Array.
(* -------------------------------------------------------------------------- *)
Hint Extern 1 (RegisterSpec Array_ml.make) => Provide make_spec.
Hint Extern 1 (RegisterSpec Array_ml.get) => Provide get_spec.
Hint Extern 1 (RegisterSpec Array_ml.set) => Provide set_spec.
Hint Extern 1 (RegisterSpec Array_ml.length) => Provide length_spec.
Hint Extern 1 (RegisterSpec Array_ml.copy) => Provide copy_spec.
Hint Extern 1 (RegisterSpec Array_ml.fill) => Provide fill_spec.
Hint Extern 1 (RegisterSpec Array_ml.iter) => Provide iter_spec.
(* [Array.of_list]. *)
Parameter of_list_spec :
curried 2%nat Array_ml.of_list /\
forall A (xs:list A),
app Array_ml.of_list [xs]
PRE \[]
POST (fun t => t ~> Array xs).
Hint Extern 1 (RegisterSpec Array_ml.of_list) => Provide of_list_spec.
(* -------------------------------------------------------------------------- *)
(* [Array.sub]. *)
Parameter sub_spec :
curried 3%nat Array_ml.sub /\
forall A `{Inhab A} (xs:list A) t ofs len,
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]]).
Hint Extern 1 (RegisterSpec Array_ml.sub) => Provide sub_spec.
(* TEMPORARY todo: define [LibListZ.sub] at the logical level *)
*)
\ No newline at end of file
(************************************************************)
(************************************************************)
(************************************************************)
(** 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.
*)
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