Commit d0c6f75e authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix some examples with model types.

parent f4b952ef
......@@ -68,7 +68,7 @@ module HashTable
use import int.Int
use import map.Map
type t 'a 'b model { mutable contents: map 'a (option 'b) }
type t 'a 'b = private { ghost mutable contents: map 'a (option 'b) }
function ([]) (h: t 'a 'b) (k: 'a) : option 'b = Map.get h.contents k
......@@ -95,12 +95,10 @@ module MaxMatrixMemo
use import map.Map
use map.Const
use import ref.Ref
constant n : int
axiom n_nonneg: 0 <= n
use import Bitset
axiom integer_size: n <= size
val constant n : int
ensures { 0 <= result <= size }
constant m : map int (map int int)
axiom m_pos: forall i j: int. 0 <= i < n -> 0 <= j < n -> 0 <= m[i][j]
......
......@@ -5,11 +5,15 @@ module ResizableArraySpec
use import map.Map
use map.Const
type rarray 'a model { mutable length: int; mutable data: map int 'a }
type rarray 'a = private {
ghost mutable length: int;
ghost mutable data: map int 'a
}
function ([]) (r: rarray 'a) (i: int) : 'a = Map.get r.data i
function ([<-]) (r: rarray 'a) (i: int) (v: 'a) : rarray 'a =
{ r with data = Map.set r.data i v }
val function ([<-]) (r: rarray 'a) (i: int) (v: 'a) : rarray 'a
ensures { result.length = r.length }
ensures { result.data = Map.set r.data i v }
val make (len: int) (dummy: 'a) : rarray 'a
requires { 0 <= len }
......@@ -17,9 +21,6 @@ module ResizableArraySpec
ensures { result.data = Const.const dummy }
(* ensures { forall i: int. 0 <= i < len -> result[i] = dummy } *)
val length (r: rarray 'a) : int
ensures { result = r.length }
val ([]) (r: rarray 'a) (i: int) : 'a
requires { 0 <= i < r.length } ensures { result = r[i] }
......@@ -48,13 +49,11 @@ module ResizableArrayImplem (* : ResizableArraySpec *)
type rarray 'a =
{ dummy: 'a; mutable length: int; mutable data: A.array 'a }
invariant { 0 <= self.length <= A.length self.data }
invariant { forall i: int. self.length <= i < A.length self.data ->
A.get self.data i = self.dummy }
invariant { 0 <= length <= A.length data }
invariant { forall i: int. length <= i < A.length data ->
A.([]) data i = dummy }
function ([]) (r: rarray 'a) (i: int) : 'a = A.get r.data i
function ([<-]) (r: rarray 'a) (i: int) (v: 'a) : rarray 'a =
{ r with data = A.set r.data i v }
function ([]) (r: rarray 'a) (i: int) : 'a = A.([]) r.data i
(*
function make (len: int) (dummy: 'a) : rarray 'a =
......@@ -65,17 +64,18 @@ function make (len: int) (dummy: 'a) : rarray 'a =
requires { 0 <= len }
ensures { result.dummy = dummy }
ensures { result.length = len }
ensures { forall i:int. 0 <= i < len -> A.get result.data i = dummy }
ensures { forall i:int. 0 <= i < len -> A.([]) result.data i = dummy }
=
{ dummy = dummy; length = len; data = A.make len dummy }
let ([]) (r: rarray 'a) (i: int) : 'a
requires { 0 <= i < r.length } ensures { result = r[i] }
requires { 0 <= i < r.length }
=
A.([]) r.data i
let ([]<-) (r: rarray 'a) (i: int) (v: 'a) : unit
requires { 0 <= i < r.length } ensures { r = (old r)[i <- v] }
requires { 0 <= i < r.length }
ensures { r.data.A.elts = A.M.([<-]) (old r).data.A.elts i v }
=
A.([]<-) r.data i v
......
......@@ -40,7 +40,7 @@ module UnionFind_sig
use import int.Int
use export UnionFind_pure
type uf model { mutable state : uf_pure }
type uf = private { ghost mutable state : uf_pure }
val create (n:int) : uf
requires { 0 <= n }
......
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