Commit f4bca762 authored by charguer's avatar charguer
Browse files

renaming

parent 0db2fb70
......@@ -24,10 +24,10 @@ Proof using.
Qed.
Module Export MArray.
Module ArrayMap.
Parameter MArray : forall A, map int A -> loc -> hprop.
Parameter ArrayMap : forall A, map int A -> loc -> hprop.
Import TLC.LibSet.
Open Scope set_scope.
......@@ -35,8 +35,8 @@ Open Scope set_scope.
Definition conseq_dom A (n:int) (M:map int A) : Prop :=
dom M = \set{ i | 0 <= i < n }.
Parameter MArray_conseq_dom : forall A (M:map int A) p,
p ~> MArray M ==+> Hexists n, \[conseq_dom n M].
Parameter ArrayMap_conseq_dom : forall A (M:map int A) p,
p ~> ArrayMap M ==+> Hexists n, \[conseq_dom n M].
(*******************************************************************)
......@@ -70,7 +70,7 @@ Qed.
(* TODO: MArray domain *)
(* TODO: ArrayMap domain *)
(* -------------------------------------------------------------------------- *)
......@@ -95,7 +95,7 @@ Parameter get_spec :
forall A `{Inhab A} (xs:map int A) t i,
index xs i ->
app Array_ml.get [t i]
INV (t ~> MArray xs)
INV (t ~> ArrayMap xs)
POST \[= xs[i] ].
Hint Extern 1 (RegisterSpec Array_ml.get) => Provide get_spec.
......@@ -109,8 +109,8 @@ Parameter set_spec :
forall A (xs:map int A) t (i:int) (x:A),
index xs i ->
app Array_ml.set [t i x]
PRE ( t ~> MArray xs)
POST (# t ~> MArray (xs[i:=x])).
PRE ( t ~> ArrayMap xs)
POST (# t ~> ArrayMap (xs[i:=x])).
Hint Extern 1 (RegisterSpec Array_ml.set) => Provide set_spec.
......@@ -124,7 +124,7 @@ Parameter make_spec :
0 <= n ->
app Array_ml.make [n x]
PRE \[]
POST (fun t => Hexists xs, t ~> MArray xs \* \[xs = make n x]).
POST (fun t => Hexists xs, t ~> ArrayMap xs \* \[xs = make n x]).
Hint Extern 1 (RegisterSpec Array_ml.make) => Provide make_spec.
*)
......@@ -144,13 +144,13 @@ Axiom init_spec :
app Array_ml.init [n f]
PRE \[]
POST (fun t =>
Hexists (xs:map int A), t ~> MArray xs \* \[conseq_dom n xs]
Hexists (xs:map int A), t ~> ArrayMap xs \* \[conseq_dom n xs]
\* \[forall i, index xs i -> xs[i] = F i]).
Hint Extern 1 (RegisterSpec Array_ml.init) => Provide init_spec.
End MArray.
End ArrayMap.
......
Set Implicit Arguments.
Require Import UF.
Require Import ArrayMap.
Require Import UFArray_ml.
Implicit Type P : map int int.
......
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