Commit a5e89797 authored by MARCHE Claude's avatar MARCHE Claude

New post for Array.make, updated examples that need Const.const

parent 53872de5
......@@ -119,7 +119,9 @@ theory array.Array
syntax function length "(size %1 : int)"
syntax function elts "(get %1)"
syntax function set "(set %1 %2 %3)"
(* does not exist anymore
syntax function make "(make %1 %2)"
*)
end
......@@ -132,6 +134,8 @@ theory matrix.Matrix
syntax function columns "(ncols %1 : int)"
syntax function elts "(matrix_get_curry %1)"
syntax function set "(matrix_set %1 %2 %3)"
(* does not exist anymore
syntax function make "(matrix_make %1 %2)"
*)
end
......@@ -50,6 +50,7 @@ module ResizableArraySpec
use import int.Int
use import map.Map
use map.Const
type rarray 'a model { mutable length: int; mutable data: map int 'a }
......@@ -63,7 +64,7 @@ module ResizableArraySpec
val make (len: int) (dummy: ~'a) : rarray 'a
requires { 0 <= len }
ensures { result.length = len }
ensures { result.data = Map.const dummy }
ensures { result.data = Const.const dummy }
val ([]) (r: rarray ~'a) (i: int) : 'a
requires { 0 <= i < r.length }
......
......@@ -123,6 +123,7 @@ end
module BellmanFord
use import map.Map
use map.Const
use import Graph
use int.IntInf as D
......@@ -132,7 +133,7 @@ module BellmanFord
type distmap = map vertex D.t
function initialize_single_source (s: vertex) : distmap =
(const D.Infinite)[s <- D.Finite 0]
(Const.const D.Infinite)[s <- D.Finite 0]
(* [inv1 m pass via] means that we already performed [pass-1] steps
of the main loop, and, in step [pass], we already processed edges
......
......@@ -12,6 +12,7 @@ module HashtblImpl
use import list.List
use import list.Mem
use import map.Map
use map.Const
use import array.Array
type key
......@@ -47,17 +48,17 @@ module HashtblImpl
let create (n: int) : t 'a
requires { 1 <= n }
ensures { result.view = Map.const None }
ensures { result.view = Const.const None }
=
{ size = 0; data = make n Nil; view = Map.const None }
{ size = 0; data = make n Nil; view = Const.const None }
let clear (h: t 'a) : unit
writes { h.size, h.data.elts, h.view }
ensures { h.view = Map.const None }
ensures { h.view = Const.const None }
=
h.size <- 0;
fill h.data 0 (length h.data) Nil;
h.view <- Map.const None
h.view <- Const.const None
let resize (h: t 'a) : unit
writes { h.data }
......
......@@ -202,8 +202,9 @@ end
theory TestSemantics
use import SemOp
use map.Const
function my_sigma : env = IdMap.const (Vint 0)
function my_sigma : env = Const.const (Vint 0)
constant x : ident
constant y : mident
......
......@@ -44,11 +44,11 @@ function eval (f:prop_fmla) (v:idmap bool) : bool =
end
use map.Const
goal Test1 :
let x = mk_ident 0 in
let v = IdMap.set (IdMap.const False) x True in
let v = IdMap.set (Const.const False) x True in
eval (For (Fnot (Fatom x)) (Ffalse)) v = False
end
......@@ -56,18 +56,20 @@ function eval_expr (s:state) (e:expr) : int =
eval_bin (eval_expr s e1) op (eval_expr s e2)
end
use map.Const
goal Test13 :
let s = IdMap.const 0 in
let s = Const.const 0 in
eval_expr s (Econst 13) = 13
goal Test42 :
let x = mk_ident 0 in
let s = IdMap.set (IdMap.const 0) x 42 in
let s = IdMap.set (Const.const 0) x 42 in
eval_expr s (Evar x) = 42
goal Test55 :
let x = mk_ident 0 in
let s = IdMap.set (IdMap.const 0) x 42 in
let s = IdMap.set (Const.const 0) x 42 in
eval_expr s (Ebin (Evar x) Oplus (Econst 13)) = 55
......@@ -111,14 +113,14 @@ inductive one_step state stmt state stmt =
goal Ass42 :
let x = mk_ident 0 in
let s = IdMap.const 0 in
let s = Const.const 0 in
forall s':state.
one_step s (Sassign x (Econst 42)) s' Sskip ->
IdMap.get s' x = 42
goal If42 :
let x = mk_ident 0 in
let s = IdMap.const 0 in
let s = Const.const 0 in
forall s1 s2:state, i:stmt.
one_step s
(Sif (Evar x)
......@@ -250,5 +252,3 @@ Local Variables:
compile-command: "why3ide imp_n.why"
End:
*)
......@@ -262,9 +262,10 @@ end
theory TestSemantics
use import Imp
use map.Const
function my_sigma : env = IdMap.const (Vint 0)
function my_pi : env = IdMap.const (Vint 42)
function my_sigma : env = Const.const (Vint 0)
function my_pi : env = Const.const (Vint 42)
goal Test13 :
eval_term my_sigma my_pi (Tconst 13) = Vint 13
......@@ -459,4 +460,3 @@ Local Variables:
compile-command: "why3ide wp2.mlw"
End:
*)
......@@ -70,6 +70,7 @@ module N
else 0
use map.MapEq
use map.Const
let rec lemma value_sub_frame (x y:map int limb) (n m:int)
requires { MapEq.map_eq_sub x y n m }
......@@ -111,7 +112,7 @@ module N
value_sub_concat (Map.set x i v) n i m
let rec lemma value_zero (x:map int limb) (n m:int)
requires { MapEq.map_eq_sub x (Map.const Limb.zero_unsigned) n m }
requires { MapEq.map_eq_sub x (Const.const Limb.zero_unsigned) n m }
variant { m - n }
ensures { value_sub x n m = 0 }
= if n < m then value_zero x (n+1) m else ()
......@@ -143,7 +144,7 @@ module N
requires { p2i l > p2i x.digits.length }
writes { x }
ensures { x.digits.length = l }
ensures { MapEq.map_eq_sub x.digits.elts (Map.const Limb.zero_unsigned)
ensures { MapEq.map_eq_sub x.digits.elts (Const.const Limb.zero_unsigned)
(p2i (old x).digits.length) (p2i l) }
ensures { value x = value (old x) }
= 'Init:
......@@ -151,11 +152,11 @@ module N
let zero = Int31.of_int 0 in
let lx = x.digits.length in
let r = Array31.make l limb_zero in
assert { MapEq.map_eq_sub r.elts (Map.const limb_zero) (p2i lx) (p2i l) };
assert { MapEq.map_eq_sub r.elts (Const.const limb_zero) (p2i lx) (p2i l) };
Array31.blit x.digits zero r zero lx;
assert { MapEq.map_eq_sub x.digits.elts r.elts 0 (p2i lx) };
assert { value_sub x.digits.elts 0 (p2i lx) = value (at x 'Init) };
assert { MapEq.map_eq_sub r.elts (Map.const limb_zero) (p2i lx) (p2i l) };
assert { MapEq.map_eq_sub r.elts (Const.const limb_zero) (p2i lx) (p2i l) };
assert { value_sub r.elts (p2i lx) (p2i l) = 0 };
assert { value_sub r.elts 0 (p2i l) = value_sub r.elts 0 (p2i lx)
+ value_sub r.elts (p2i lx) (p2i l) * power radix (p2i lx) };
......@@ -506,7 +507,7 @@ module N
let ly = y.digits.length in
if Int31.(>) lx (Int31.(-) (of_int 0x3FFFFFFF) ly) then raise TooManyDigits;
let zd = Array31.make (Int31.(+) lx ly) limb_zero in
assert { MapEq.map_eq_sub zd.elts (Map.const limb_zero) 0 (p2i lx + p2i ly) };
assert { MapEq.map_eq_sub zd.elts (Const.const limb_zero) 0 (p2i lx + p2i ly) };
assert { value_sub zd.elts 0 (p2i lx + p2i ly) = 0 };
let _c = mul_limbs zd x.digits y.digits zero zero lx zero ly in
assert { l2i _c = 0 };
......
......@@ -35,6 +35,7 @@ module LinearProbing
use import option.Option
use import list.Mem
use import map.Map
use map.Const
use import ref.Ref
use import array.Array
......@@ -118,7 +119,7 @@ module LinearProbing
ensures { forall x: key. not (Map.get result.view (keym x)) }
=
{ size = 0; data = Array.make n dummy;
view = Map.const false; loc = Map.const 0; }
view = Const.const false; loc = Const.const 0; }
let clear (h: t) : unit
writes { h.size, h.data.elts, h.view }
......@@ -127,7 +128,7 @@ module LinearProbing
=
h.size <- 0;
Array.fill h.data 0 (Array.length h.data) dummy;
h.view <- Map.const false
h.view <- Const.const false
function next (n i: int) : int =
let i = i+1 in if i = n then 0 else i
......@@ -173,7 +174,7 @@ module LinearProbing
let n = Array.length h.data in
let n2 = 2 * n in
let a = Array.make n2 dummy in
let ghost l = ref (Map.const 0) in
let ghost l = ref (Const.const 0) in
for i = 0 to n - 1 do
invariant { numofd a 0 n2 = numofd h.data 0 i + n2 - i }
invariant { forall j: int. 0 <= j < n2 -> neq a[j] dummy ->
......@@ -321,5 +322,3 @@ module LinearProbing
end
end
......@@ -93,6 +93,7 @@ module MaxMatrixMemo
use import int.Int
use import int.MinMax
use import map.Map
use map.Const
use import ref.Ref
constant n : int
......@@ -149,10 +150,10 @@ module MaxMatrixMemo
requires { pre (i, c) /\ inv table }
ensures { post (i,c) result /\ inv table }
= if i = n then
(0, const 0)
(0, Const.const 0)
else begin
let r = ref (-1) in
let sol = ref (const 0) in
let sol = ref (Const.const 0) in
for j = 0 to n-1 do
invariant {
inv table /\
......
......@@ -3,6 +3,7 @@ module ResizableArraySpec
use import int.Int
use import map.Map
use map.Const
type rarray 'a model { mutable length: int; mutable data: map int 'a }
......@@ -13,7 +14,7 @@ module ResizableArraySpec
val make (len: int) (dummy: 'a) : rarray 'a
requires { 0 <= len }
ensures { result.length = len }
ensures { result.data = Map.const dummy }
ensures { result.data = Const.const dummy }
(* ensures { forall i: int. 0 <= i < len -> result[i] = dummy } *)
val length (r: rarray 'a) : int
......@@ -55,11 +56,16 @@ module ResizableArrayImplem (* : ResizableArraySpec *)
function ([<-]) (r: rarray 'a) (i: int) (v: 'a) : rarray 'a =
{ r with data = A.set r.data i v }
function make (len: int) (dummy: 'a) : rarray 'a =
(*
function make (len: int) (dummy: 'a) : rarray 'a =
{ dummy = dummy; length = len; data = A.make len dummy }
*)
let make (len: int) (dummy: 'a) : rarray 'a
requires { 0 <= len } ensures { result = make len dummy }
requires { 0 <= len }
ensures { result.dummy = dummy }
ensures { result.length = len }
ensures { forall i:int. 0 <= i < len -> A.get result.data i = dummy }
=
{ dummy = dummy; length = len; data = A.make len dummy }
......
......@@ -614,6 +614,7 @@ module Test
use import Solver
use array.Array
use import map.Map
use map.Const
(** Solving the empty grid: easy, yet not trivial *)
let test0 ()
......@@ -645,7 +646,7 @@ module Test
0 0 0 0 0 0 0 7 6
*)
constant solvable : grid =
(const 0)
(Const.const 0)
[0<-2][2<-9][7<-1]
[13<-6]
[19<-5][20<-3][21<-8][23<-2][24<-7]
......
......@@ -49,6 +49,7 @@ module Static
use import Graph
use set.Fset as S
use map.Map as M
use map.Const
function defined_sort (m:msort) : S.set vertex
axiom defined_sort_def:
......@@ -110,7 +111,7 @@ module Static
=
'Init:
let next = ref 0 in
let values = ref (M.const (-1)) in
let values = ref (Const.const (-1)) in
let p = ref (vertices g) in
while not (S.is_empty !p) do
invariant { inv g !values !next }
......@@ -155,6 +156,7 @@ module Online_Basic
use import Online_graph
use set.Fset as S
use map.Map as M
use map.Const
type marked = (S.set vertex)
......@@ -172,7 +174,7 @@ module Online_Basic
ensures { result.graph = g }
ensures { inv result }
=
{graph = g; values = M.const 0}
{graph = g; values = Const.const 0}
let rec dfs (g:t) (v:vertex)
(seen:marked) (min_depth:int) : unit
......
......@@ -15,11 +15,12 @@ lemma Is_heap_min:
is_heap_array a 0 n -> a[0] = min_bag (model (a, n))
use import ref.Ref
use map.Const
(* implementation of heaps *)
let create () : ref logic_heap
ensures { is_heap !result /\ model !result = empty_bag }
= let x = (A.const 0, 0) in ref x
= let x = (Const.const 0, 0) in ref x
exception Break
......
......@@ -49,17 +49,10 @@ module Array
= if i < 0 || i >= length a then raise OutOfBounds;
a[i] <- v
function make (n: int) (v: ~'a) : array 'a
axiom make_length:
forall n:int, v:'a. length (make n v) = n
axiom make_elts:
forall n i:int, v:'a. get (make n v) i = v
val make (n: int) (v: ~'a) : array 'a
requires { "expl:array creation size" n >= 0 }
ensures { length result = n }
ensures { forall i:int. result[i] = v }
ensures { forall i:int. 0 <= i < n -> result[i] = v }
val append (a1: array ~'a) (a2: array 'a) : array 'a
ensures { length result = length a1 + length a2 }
......
......@@ -50,15 +50,10 @@ module Array32
= if i < of_int 0 || i >= length a then raise OutOfBounds;
a[i] <- v
function make (n: int32) (v: ~'a) : array 'a
axiom make_length:
forall n:int32, v:'a. length (make n v) = n
axiom make_elts:
forall n:int32, i:int, v:'a. get (make n v) i = v
val make (n: int32) (v: ~'a) : array 'a
requires { "expl:array creation size" to_int n >= 0 }
ensures { forall i:int. get result i = v }
ensures { length result = n }
ensures { forall i:int. 0 <= i < to_int n -> get result i = v }
val append (a1: array ~'a) (a2: array 'a) : array 'a
ensures { to_int result.length = to_int a1.length + to_int a2.length }
......@@ -170,15 +165,10 @@ module Array31
= if i < of_int 0 || i >= length a then raise OutOfBounds;
a[i] <- v
function make (n: int31) (v: ~'a) : array 'a
axiom make_length:
forall n:int31, v:'a. length (make n v) = n
axiom make_elts:
forall n:int31, i:int, v:'a. get (make n v) i = v
val make (n: int31) (v: ~'a) : array 'a
requires { "expl:array creation size" to_int n >= 0 }
ensures { forall i:int. get result i = v }
ensures { length result = n }
ensures { forall i:int. 0 <= i < to_int n -> get result i = v }
val append (a1: array ~'a) (a2: array 'a) : array 'a
ensures { to_int result.length = to_int a1.length + to_int a2.length }
......@@ -290,15 +280,10 @@ module Array63
= if i < of_int 0 || i >= length a then raise OutOfBounds;
a[i] <- v
function make (n: int63) (v: ~'a) : array 'a
axiom make_length:
forall n:int63, v:'a. length (make n v) = n
axiom make_elts:
forall n:int63, i:int, v:'a. get (make n v) i = v
val make (n: int63) (v: ~'a) : array 'a
requires { "expl:array creation size" to_int n >= 0 }
ensures { forall i:int. get result i = v }
ensures { length result = n }
ensures { forall i:int. 0 <= i < to_int n -> get result i = v }
val append (a1: array ~'a) (a2: array 'a) : array 'a
ensures { to_int result.length = to_int a1.length + to_int a2.length }
......
......@@ -50,14 +50,11 @@ module Matrix
if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
set a i v
function make (r c: int) (v: 'a) : matrix 'a
axiom make_rows: forall r c, v:'a. (make r c v).rows = r
axiom make_columns: forall r c, v:'a. (make r c v).columns = c
axiom make_elts: forall r c, v:'a, i j. get (make r c v) (i,j) = v
val make (r c: int) (v: 'a) : matrix 'a
requires { r >= 0 /\ c >= 0 }
ensures { result = make r c v }
ensures { result.rows = r }
ensures { result.columns = c }
ensures { forall i j. 0 <= i < r /\ 0 <= j < c -> get result (i,j) = v }
val copy (a: matrix 'a) : matrix 'a
ensures { result.rows = a.rows /\ result.columns = a.columns }
......
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