modules: stdlib split in files ref and array

parent e62f3515
module M
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
parameter incr : x:ref int -> { } unit writes x { x = old x + 1 }
......
......@@ -2,7 +2,7 @@ module M
exception Exception int
use import module stdlib.Ref
use import module ref.Ref
parameter t : ref int
......
module M
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
exception Break
......
......@@ -43,7 +43,7 @@ let p6 () =
(* composition of exceptions with side-effect on a reference *)
use import module stdlib.Ref
use import module ref.Ref
parameter x : ref int
......
module M
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
(* for loop with invariant *)
let test1 () =
......
module M
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
(** 1. A loop increasing [i] up to 10. *)
......
module M
use import module stdlib.Ref
use import module ref.Ref
logic q1 int int int
......
module M
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
(* Tests for proof obligations. *)
......
module M
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
(** Recursive functions *)
......
module M
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
(* Side effect in expressions (Bart Jacobs' tricky example) *)
......
module M
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
(* side effects in tests *)
......
module M
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
parameter x : ref int
......
......@@ -15,9 +15,9 @@ Pages: 321 - 322
module Algo63
use import int.Int
use import module stdlib.Ref
use import module stdlib.Array
use import module stdlib.ArrayPermut
use import module ref.Ref
use import module array.Array
use import module array.ArrayPermut
parameter partition :
a : array int -> m:int -> n:int -> i:ref int -> j:ref int ->
......
......@@ -15,13 +15,13 @@ Pages: 321 - 322
module Algo64
use import int.Int
use import module stdlib.Ref
use import module stdlib.Array
use import module stdlib.ArrayPermut
use import module ref.Ref
use import module array.Array
use import module array.ArrayPermut
logic sorted_sub (a: array int) (l u: int)
(*
clone import module stdlib.ArraySorted with type elt = int, logic le = (<=)
clone import module array.ArraySorted with type elt = int, logic le = (<=)
*)
(* Algorithm 63 *)
......
......@@ -15,9 +15,9 @@ Pages: 321 - 322
module Algo65
use import int.Int
use import module stdlib.Ref
use import module stdlib.Array
use import module stdlib.ArrayPermut
use import module ref.Ref
use import module array.Array
use import module array.ArrayPermut
(* algorithm 63 *)
......
......@@ -3,8 +3,8 @@
module M
use import module stdlib.Refint
use import module stdlib.Array
use import module ref.Refint
use import module array.Array
parameter a : array int
......@@ -44,7 +44,7 @@ module ARM
use export int.Int
use export map.Map
use export module stdlib.Ref
use export module ref.Ref
(* memory *)
parameter mem : ref (map int int)
......
......@@ -6,8 +6,8 @@ module M
use import int.Int
use import int.ComputerDivision
use import module stdlib.Ref
use import module stdlib.Array
use import module ref.Ref
use import module array.Array
(* the code and its specification *)
......
......@@ -21,7 +21,7 @@ module M1
use import int.Int
use import int.ComputerDivision
use import module stdlib.Ref
use import module ref.Ref
type pointer
type memory
......@@ -67,7 +67,7 @@ module M2
use import int.Int
use import int.ComputerDivision
use import module stdlib.Ref
use import module ref.Ref
type pointer
type memory
......@@ -115,7 +115,7 @@ module M3
use import int.Int
use import int.ComputerDivision
use import module stdlib.Ref
use import module ref.Ref
type int32
logic to_int int32 : int
......
......@@ -3,7 +3,7 @@
module M
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
(* Parameters.
Without loss of generality, we can take [x1=0] and [y1=0].
......
module M
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
(* preliminaries *)
......
......@@ -8,8 +8,8 @@
module Decrease1
use import int.Int
use import module stdlib.Ref
use import module stdlib.Array
use import module ref.Ref
use import module array.Array
logic decrease1 (a: array int) =
forall i: int. 0 <= i < length a - 1 -> a[i+1] >= a[i] - 1
......
module M
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
use set.Fset as S
use map.Map as M
......
......@@ -17,8 +17,8 @@ module Distance
use import int.Int
use import int.MinMax
use import list.List
use import module stdlib.Ref
use import module stdlib.Array
use import module ref.Ref
use import module array.Array
(* Parameters. Input of the program is composed of two arrays
of characters, [w1] of size [n1] and [w2] of size [n2]. *)
......
......@@ -92,7 +92,7 @@ end
module Solve
use import module stdlib.Ref
use import module ref.Ref
use import FibOnlyEven
let f m : int =
......
......@@ -3,7 +3,7 @@
module M
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
logic fib int : int
......
......@@ -26,7 +26,7 @@ module FibonacciLinear
use import Fibonacci
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
let fib (n:int) : int =
{ n >= 0 }
......
......@@ -3,9 +3,9 @@
module Flag
use import int.Int
use import module stdlib.Ref
use import module stdlib.Array
use import module stdlib.ArrayPermut
use import module ref.Ref
use import module array.Array
use import module array.ArrayPermut
type color = Blue | White | Red
......
......@@ -3,7 +3,7 @@ module M
use import int.Int
use import int.ComputerDivision
use import int.Gcd
use import module stdlib.Ref
use import module ref.Ref
let gcd (x:int) (y:int) =
{ x >= 0 and y >= 0 }
......
......@@ -4,7 +4,7 @@
module M
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
logic sqr (x:int) : int = x * x
......
......@@ -2,7 +2,7 @@
module M
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
use import map.Map
type pointer
......
......@@ -17,7 +17,7 @@ module M
(* non-recursive implementation using a while loop *)
use import module stdlib.Ref
use import module ref.Ref
logic f (x: int) : int =
if x >= 101 then x-10 else 91
......
......@@ -2,8 +2,8 @@
module Muller
use import int.Int
use import module stdlib.Refint
use import module stdlib.Array
use import module ref.Refint
use import module array.Array
type param = M.map int int
logic pr (a : param) (n : int) = M.get a n <> 0
......
......@@ -10,8 +10,8 @@ module M
*)
use import int.Int
use import module stdlib.Ref
use import module stdlib.Array
use import module ref.Ref
use import module array.Array
use import int.MinMax
use import int.EuclideanDivision
use import int.Power
......
......@@ -39,7 +39,7 @@ module M
(* non-recursive implementation using a while loop *)
use import module stdlib.Ref
use import module ref.Ref
let fast_exp_imperative x n =
{ 0 <= n }
......
......@@ -8,11 +8,11 @@
module Quicksort
use import int.Int
use import module stdlib.Ref
use import module stdlib.Array
use import module stdlib.ArraySorted
use import module stdlib.ArrayPermut
use import module stdlib.ArrayEq
use import module ref.Ref
use import module array.Array
use import module array.ArraySorted
use import module array.ArrayPermut
use import module array.ArrayEq
let swap (t:array int) (i:int) (j:int) =
{ 0 <= i < length t and 0 <= j < length t }
......
......@@ -37,7 +37,7 @@ module Relabel
same_shape (Node l1 r1) (Node l2 r2)
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
parameter r : ref int
......
......@@ -9,7 +9,7 @@
module HoareLogic
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
(* Example: Slow Subtraction *)
......@@ -96,7 +96,7 @@ end
module MoreHoareLogic
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
use import list.List
use import list.HdTl
use import list.Length
......
......@@ -5,7 +5,7 @@ module M
(* answer: 20444710234716473 *)
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
use import int.EuclideanDivision
use import int.Power
......
......@@ -31,7 +31,7 @@ end
module UnionFind_sig
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
use export UnionFind
......@@ -75,10 +75,8 @@ theory Graph
type graph
inductive path graph vertex vertex =
| Path_refl :
forall g:graph, x:vertex. path g x x
| Path_sym :
forall g:graph, x y:vertex. path g x y -> path g y x
| Path_refl : forall g:graph, x:vertex. path g x x
| Path_sym : forall g:graph, x y:vertex. path g x y -> path g y x
| Path_trans:
forall g:graph, x y z:vertex. path g x y -> path g y z -> path g x z
......@@ -93,11 +91,10 @@ end
module Graph_sig
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
clone export Graph with type vertex = int
(* use export Graph *)
(* use export Graph_int*)
(* clone export Graph with type vertex = int *)
use export Graph_int
parameter graph : ref graph
......@@ -119,7 +116,7 @@ end
module BuildMaze
use import int.Int
use import module stdlib.Ref
use import module ref.Ref
use import module UnionFind_sig
use import module Graph_sig
......@@ -129,7 +126,7 @@ module BuildMaze
lemma Ineq1 :
forall n x y:int. 0 <= n -> 0 <= x < n -> 0 <= y < n -> 0 <= x*n+y < n*n
let add_edge_and_union u (a:int) (b:int) =
let add_edge_and_union (u: ref uf) (a:int) (b:int) =
{ 0 <= a < size u and 0 <= b < size u and
not same u a b and not path graph a b and
forall x y:int.
......
module M
use import module stdlib.Ref
use import module ref.Ref
(* Red-black trees (data type) *)
......
module M
use import module stdlib.Ref
use import module ref.Ref
type key = int
type value = int
......
......@@ -21,8 +21,8 @@ back +-+-+-+-------------------+
*)
use import int.Int
use import module stdlib.Ref
use array.ArrayLength as A
use import module ref.Ref
use import module array.Array as A
logic maxlen : int = 1000
......@@ -31,31 +31,28 @@ back +-+-+-+-------------------+
logic c1 : elt
logic c2 : elt
type array 'a = A.t int 'a
type sparse_array = {| val : array elt;
idx : array int;
back : array int;
mutable card : int; |}
logic (#) (a : array 'a) (i : int) : 'a = A.get a i
logic length (a: sparse_array) : int = A.length a.val
type sparse_array = SA (sa_val : array elt)
(sa_idx : array int)
(sa_back : array int)
(sa_sz : int)
(sa_n : int)
logic is_elt (a : sparse_array) (i : int) =
let (SA val idx back _ n) = a in
0 <= idx#i < n and back#(idx#i) = i
logic is_elt (a: sparse_array) (i: int) =
0 <= a.idx[i] < a.card and a.back[a.idx[i]] = i
logic model (a : sparse_array) (i : int) : elt =
if is_elt a i then
(sa_val a)#i
a.val[i]
else
default
logic invariant_ (a : sparse_array) =
let (SA val idx back sz n) = a in
0 <= n <= sz <= maxlen and
A.length val = sz and A.length idx = sz and A.length back = sz and
forall i : int. 0 <= i < n -> 0 <= back#i < sz and idx#(back#i) = i
0 <= a.card <= length a <= maxlen and
A.length a.val = A.length a.idx = A.length a.back and
forall i : int.
0 <= i < a.card ->
0 <= a.back[i] < length a and a.idx[a.back[i]] = i
(*
The following definitions and the axiom Dirichlet
......@@ -64,9 +61,9 @@ back +-+-+-+-------------------+
the proof of WPs for the function [set] below.
*)
logic permutation (n : int) (a : array int) =
(forall i : int. 0 <= i < n -> 0 <= a#i < n) and
(forall i j : int. 0 <= i < j < n -> a#i <> a#j)
logic permutation (n: int) (a: array int) =
(forall i : int. 0 <= i < n -> 0 <= a[i] < n) and
(forall i j : int. 0 <= i < j < n -> a[i] <> a[j])
logic dirichlet (n : int) (a : array int) (i : int) : int
......@@ -76,47 +73,42 @@ back +-+-+-+-------------------+
permutation n a ->
(forall i : int. 0 <= i < n ->
0 <= dirichlet n a i < n and
a # dirichlet n a i = i)
a[dirichlet n a i] = i)
lemma Inter6 :
forall a : sparse_array . invariant_ a ->
let (SA val idx back sz n) = a in
n = sz ->
permutation sz back &&
forall i : int. 0 <= i < sz ->
idx#i = dirichlet sz back i && is_elt a i
a.card = length a ->
permutation a.card a.back &&
forall i : int. 0 <= i < a.card ->
a.idx[i] = dirichlet a.card a.back i && is_elt a i
(*
parameter create :
sz:int ->
{ 0 <= sz <= maxlen }
ref sparse_array
{ sa_sz !result = sz and forall i:int. model !result i = default }
*)
sparse_array
{ invariant_ result and
result.card = 0 and
length result = sz and forall i:int. model result i = default }
(*
parameter malloc : n:int -> {} array 'a { A.length result = n }
let create sz =
{ 0 <= sz <= maxlen }
ref (SA (malloc sz) (malloc sz) (malloc sz) sz 0)
Mk_sparse_array (malloc sz) (malloc sz) (malloc sz) 0
{ invariant_ result and
sa_sz result = sz and forall i:int. model result i = default }
*)
let array_get (a : array 'a) i =
{ 0 <= i < A.length a } A.get a i { result = A.get a i }
let array_set (a : array 'a) i v =
{ 0 <= i < A.length a } A.set a i v { result = A.set a i v }
let test (a : ref sparse_array) i =
{ 0 <= i < sa_sz a and invariant_ a }
let idx = sa_idx !a in
let back = sa_back !a in
let n = sa_n !a in
0 <= array_get idx i && array_get idx i < n &&
array_get back (array_get idx i) = i
let test (a: sparse_array) i =
{ 0 <= i < length a and invariant_ a }
let idx = idx a in
let back = back a in
let n = card a in
0 <= idx[i] && idx[i] < n && back[idx[i]] = i
{ result=True <-> is_elt a i }
(***
(*
parameter get :
a:ref sparse_array -> i:int ->
......@@ -124,11 +116,10 @@ parameter get :
elt reads a
{ result = model !a i }
*)
let get (a : ref sparse_array) i =
{ 0 <= i < sa_sz a and invariant_ a }
let val = sa_val !a in
let get (a: sparse_array) i =
{ 0 <= i < length a and invariant_ a }
if test a i then
array_get val i
array_get (val a) i
else
default
{ result = model a i }
......@@ -179,6 +170,7 @@ let harness () =
let get_a_0 = get a 0 in assert { get_a_0 = default };
let get_b_0 = get b 0 in assert { get_b_0 = default };
()
***)
end
......
module M
use import int.Int
use import module stdlib.Ref
use array.ArrayLength as A
type array 'a = A.t int 'a
logic (#) (a : array 'a) (i : int) : 'a = A.get a i
use import module ref.Ref
use import module array.Array as A
type uf = UF (link : array int)
(dist : array int) (* distance to representative *)
......@@ -15,43 +11,43 @@ module M
logic inv (u : uf) =
let UF l d s n = u in
(forall i:int. 0 <= i < s -> 0 <= l#i < s) and
(forall i:int. 0 <= i < s ->
((d#i = 0 and l#i = i) or (d#i > 0 and d#(l#i) < d#i)))
inductive repr (u:uf) (x:int) (r:int) =
| Repr_root: forall u:uf. inv u ->
forall x:int. 0 <= x < size u ->
link u #x = x -> repr u x x
| Repr_link: forall u:uf. inv u ->
forall x:int. 0 <= x < size u ->
forall r:int. repr u (link u # x) r -> repr u x r
(forall i:int. 0 <= i < s -> 0 <= l[i] < s) and
(forall i:int. 0 <= i < s ->
((d[i] = 0 and l[i] = i) or (d[i] > 0 and d[l[i]] < d[i])))
inductive repr (u:uf) (x:int) (r:int) =
| Repr_root: forall u:uf. inv u ->
forall x:int. 0 <= x < size u ->
(link u)[x] = x -> repr u x x
| Repr_link: forall u:uf. inv u ->
forall x:int. 0 <= x < size u ->
forall r:int. repr u (link u)[x] r -> repr u x r
lemma Repr_bounds_2:
forall u:uf, x y:int. repr u x y -> 0 <= y < size u
lemma Repr_dist_1:
forall u:uf, x y:int. repr u x y -> dist u # y = 0
logic same (u:uf) (x y:int) =
logic same (u:uf) (x y:int) =
forall r:int. repr u x r <-> repr u y r
logic same_reprs (u1 u2 : uf) =
logic same_reprs (u1 u2 : uf) =
forall x r:int. repr u1 x r <-> repr u2 x r
axiom OneClass :
forall u:uf. num u = 1 ->
forall u:uf. num u = 1 ->
forall x y:int. 0 <= x < size u -> 0 <= y < size u -> same u x y
let get_num_classes (u:ref uf) =
{} num !u { result = num u }
let create (n:int) =
{ 0 <= n }
{ 0 <= n }
let l = ref (A.create_const_length 0 n) in
let i = ref 0 in
while !i < n do
invariant { 0 <= i <= n and
forall j:int. 0 <= j < i -> l#j = j }
forall j:int. 0 <= j < i -> l#j = j }
variant { n - i }
l := A.set !l !i !i;
i := !i + 1
......@@ -67,11 +63,11 @@ let path_compression (u : ref uf) x r =
let l = A.set l x r in