Skip to content

GitLab

Commit 74cded5f authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

programs: refactoring of typing (in progress)

parent fd81ec38
Hide whitespace changes
Inline Side-by-side
Showing with 274 additions and 265 deletions
Makefile.in
View file @ 74cded5f
......@@ -355,6 +355,9 @@ clean::
%.gui: %.mlw bin/why3ide.opt
bin/why3ide.opt $*.mlw
%.type: %.mlw bin/why3ide.opt
bin/why3ml.opt --type-only $*.mlw
install_no_local::
cp -f bin/why3ml.@OCAMLBEST@ $(BINDIR)/why3ml
......
bin/db
View file @ 74cded5f
set arguments ../tests/test-pgm-jcf.mlw
dir ..
dir ../src
dir ../src/util
dir ../src/core
dir ../src/programs
load_printer "str.cma"
load_printer "nums.cma"
......
examples/programs/course.mlw
View file @ 74cded5f
......@@ -5,13 +5,13 @@ module M
(* preliminaries *)
use array.Array as A
use map.Map as M
type array 'a = A.t int 'a
type array 'a = M.map int 'a
logic injective (n:int) (m:int) (a:array 'a) =
forall i j:int. n <= i <= m -> n <= j <= m ->
A.get a i = A.get a j -> i = j
M.get a i = M.get a j -> i = j
type string
......@@ -19,14 +19,14 @@ module M
type pointer = int
type region 'a = A.t pointer 'a
type region 'a = M.map pointer 'a
type first_free_addr = int
logic valid (a:first_free_addr) (p:pointer) = p < a
logic valid_array (a:first_free_addr) (n:int) (m:int) (r:array pointer) =
forall i:int. n <= i <= m -> valid a (A.get r i)
forall i:int. n <= i <= m -> valid a (M.get r i)
parameter alloc : ref first_free_addr
......@@ -76,7 +76,7 @@ end
axiom MarkSumNonEmpty :
forall r:region student, i j:int, a : array pointer.
i <= j ->
let (_,mark) = A.get r (A.get a j) in
let (_,mark) = M.get r (M.get a j) in
markSum r i j a = markSum r i (j-1) a + mark
(*
......@@ -92,13 +92,13 @@ end
lemma MarkSum_set_array_outside :
forall r:region student, i j k:int, a: array pointer, p:pointer.
not (i <= k <= j) ->
markSum r i j (A.set a k p) = markSum r i j a
markSum r i j (M.set a k p) = markSum r i j a
lemma MarkSum_set_region_outside :
forall r:region student, i j:int, a: array pointer, p:pointer, s:student.
(forall k:int. i <= k <= j -> A.get a k <> p) ->
markSum (A.set r p s) i j a = markSum r i j a
(forall k:int. i <= k <= j -> M.get a k <> p) ->
markSum (M.set r p s) i j a = markSum r i j a
......@@ -128,9 +128,9 @@ fun CreateCourse(R:[Course]): [R]
let createCourse (r: (ref (region course))) : pointer =
{ }
let c = new_pointer () in
let (rStud,student,count,sum) = A.get !r c in
let (rStud,student,count,sum) = M.get !r c in
let newc = (rStud,student,0,0) in
r := A.set !r c newc;
r := M.set !r c newc;
assert { invCourse alloc newc };
c
{ valid alloc result }
......@@ -152,12 +152,12 @@ fun RegisterStudent(R:[Course], c: [R], name: string): [R.Rstud]
let registerStudent
(r: (ref (region course))) (c:pointer) (name:string) : pointer =
{ valid alloc c and invCourse alloc (A.get r c) }
{ valid alloc c and invCourse alloc (M.get r c) }
let s = new_pointer () in
let (rStud,student,count,sum) = A.get !r c in
let (rStud,student,count,sum) = M.get !r c in
let newstud = (name,0) in
let newc = (A.set rStud s newstud,A.set student count s,count+1,sum) in
r := A.set !r c newc;
let newc = (M.set rStud s newstud,M.set student count s,count+1,sum) in
r := M.set !r c newc;
assert { invCourse alloc newc };
s
{ valid alloc result }
......
examples/programs/dijkstra.mlw
View file @ 74cded5f
......@@ -3,18 +3,18 @@ module M
use import int.Int
use import module stdlib.Ref
use set.Fset as S
use array.Array as M
use map.Map as M
(* iteration on a set *)
parameter set_has_next :
s:ref (S.t 'a) ->
s:ref (S.set 'a) ->
{}
bool reads s
{ if result=True then S.is_empty s else not S.is_empty s }
parameter set_next :
s:ref (S.t 'a) ->
s:ref (S.set 'a) ->
{ not S.is_empty s }
'a writes s
{ S.mem result (old s) and s = S.remove result (old s) }
......@@ -23,9 +23,9 @@ parameter set_next :
type vertex
logic v : S.t vertex
logic v : S.set vertex
logic g_succ(vertex) : S.t vertex
logic g_succ(vertex) : S.set vertex
axiom G_succ_sound :
forall x:vertex. S.subset (g_succ x) v
......@@ -40,18 +40,18 @@ parameter eq_vertex :
(* visited vertices *)
parameter visited : ref (S.t vertex)
parameter visited : ref (S.set vertex)
parameter visited_add :
x:vertex -> {} unit writes visited { visited = S.add x (old visited) }
(* current distances *)
parameter d : ref (M.t vertex int)
parameter d : ref (M.map vertex int)
(* priority queue *)
parameter q : ref (S.t vertex)
parameter q : ref (S.set vertex)
parameter q_is_empty :
unit ->
......@@ -88,7 +88,7 @@ let relax u v =
(not S.mem v visited and not S.mem v (old q) and q = S.add v (old q) and
d = M.set (old d) v (M.get (old d) u + weight u v)) }
logic min (m:vertex) (q:S.t vertex) (d:M.t vertex int) =
logic min (m:vertex) (q:S.set vertex) (d:M.map vertex int) =
S.mem m q and
forall x:vertex. S.mem x q -> M.get d m <= M.get d x
......@@ -134,7 +134,7 @@ lemma Main_lemma :
shortest_path src v' d' and S.mem v (g_succ v') and d' + weight v' v < d
lemma Completeness_lemma :
forall s:S.t vertex. forall src:vertex. forall dst:vertex. forall d:int.
forall s:S.set vertex. forall src:vertex. forall dst:vertex. forall d:int.
(* if s is closed under g_succ *)
(forall v:vertex.
S.mem v s -> forall w:vertex. S.mem w (g_succ v) -> S.mem w s) ->
......@@ -145,10 +145,10 @@ lemma Completeness_lemma :
(* definitions used in loop invariants *)
logic inv_src (src:vertex) (s q:S.t vertex) =
logic inv_src (src:vertex) (s q:S.set vertex) =
S.mem src s or S.mem src q
logic inv (src:vertex) (s q:S.t vertex) (d:M.t vertex int) =
logic inv (src:vertex) (s q:S.set vertex) (d:M.map vertex int) =
inv_src src s q
(* S,Q are contained in V *)
and S.subset s v and S.subset q v
......@@ -167,13 +167,13 @@ logic inv (src:vertex) (s q:S.t vertex) (d:M.t vertex int) =
forall x:vertex. forall dx:int. shortest_path src x dx ->
dx < M.get d m -> S.mem x s)
logic inv_succ (src:vertex) (s q : S.t vertex) =
logic inv_succ (src:vertex) (s q : S.set vertex) =
(* successors of vertices in S are either in S or in Q *)
(forall x:vertex. S.mem x s ->
forall y:vertex. S.mem y (g_succ x) -> S.mem y s or S.mem y q)
logic inv_succ2 (src:vertex) (s q : S.t vertex)
(u:vertex) (su:S.t vertex) =
logic inv_succ2 (src:vertex) (s q : S.set vertex)
(u:vertex) (su:S.set vertex) =
(* successors of vertices in S are either in S or in Q,
unless they are successors of u still in su *)
(forall x:vertex. S.mem x s ->
......
examples/programs/distance.mlw
View file @ 74cded5f
......@@ -61,18 +61,18 @@ module Distance
logic min_dist (w1 w2:word) (n:int) =
dist w1 w2 n and forall m:int. dist w1 w2 m -> n <= m
logic suffix (map a) int : word
logic suffix (array a) int : word
axiom suffix_def_1:
forall m: map a. suffix m (length m) = Nil
forall m: array a. suffix m (length m) = Nil
axiom suffix_def_2:
forall m: map a, i: int.
forall m: array a, i: int.
0 <= i < length m -> suffix m i = Cons m[i] (suffix m (i+1))
logic min_suffix (w1 w2: map a) (i j n: int) =
logic min_suffix (w1 w2: array a) (i j n: int) =
min_dist (suffix w1 i) (suffix w2 j) n
logic word_of_array (m: map a) : word = suffix m 0
logic word_of_array (m: array a) : word = suffix m 0
(* The code. *)
......@@ -83,14 +83,14 @@ module Distance
for i = 0 to n2 do
invariant { length t = n2+1 and
forall j:int. 0 <= j < i -> t[j] = n2-j }
t[i <- n2 - i]
set t i (n2 - i)
done;
(* loop over w1 *)
for i = n1-1 downto 0 do
invariant { length t = n2+1
and forall j:int. 0 <= j <= n2 -> min_suffix w1 w2 (i+1) j t[j] }
o := t[n2];
t[n2 <- t[n2] + 1];
set t n2 (t[n2] + 1);
(* loop over w2 *)
for j = n2-1 downto 0 do
invariant { length t = n2+1
......@@ -101,9 +101,9 @@ module Distance
let temp = !o in
o := t[j];
if w1[i] = w2[j] then
t[j <- temp]
set t j temp
else
t[j <- (min t[j] t[j+1]) + 1]
set t j ((min t[j] t[j+1]) + 1)
end
done
done;
......
examples/programs/fib_memo.mlw
View file @ 74cded5f
......@@ -12,18 +12,18 @@ module M
type option 'a = None | Some 'a
use array.Array as A
use map.Map as M
type table = A.t int (option int)
type table = M.map int (option int)
logic inv (t : table) =
forall x y : int. A.get t x = Some y -> y = fib x
forall x y : int. M.get t x = Some y -> y = fib x
parameter table : ref table
parameter add :
x:int -> y:int ->
{} unit writes table { table = A.set (old table) x (Some y) }
{} unit writes table { table = M.set (old table) x (Some y) }
exception Not_found
......@@ -31,8 +31,8 @@ module M
x:int ->
{}
int reads table raises Not_found
{ A.get table x = Some result }
| Not_found -> { A.get table x = None }
{ M.get table x = Some result }
| Not_found -> { M.get table x = None }
let rec fibo n =
{ 0 <= n and inv table }
......@@ -52,6 +52,6 @@ end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/fib"
compile-command: "unset LANG; make -C ../.. examples/programs/fib_memo"
End:
*)
examples/programs/flag.mlw
View file @ 74cded5f
......@@ -5,19 +5,19 @@ module Flag
use import int.Int
use import module stdlib.Ref
use import module stdlib.Array
use import array.ArrayPermut
use import module stdlib.ArrayPermut
type color = Blue | White | Red
logic monochrome (a:map color) (i:int) (j:int) (c:color) =
logic monochrome (a:array color) (i:int) (j:int) (c:color) =
forall k:int. i<=k<j -> a[k]=c
let swap (a:array color) (i:int) (j:int) =
{ 0 <= i < length a and 0 <= j < length a }
let v = a[i] in
begin
a[i <- a[j]];
a[j <- v]
set a i a[j];
set a j v
end
{ exchange a (old a) i j }
......@@ -33,7 +33,7 @@ module Flag
monochrome a b i White and
monochrome a r n Red and
length a = n and
permut a (at a Init) 0 (n-1) }
permut_sub a (at a Init) 0 (n-1) }
variant { r - i }
match a[!i] with
| Blue ->
......@@ -51,7 +51,7 @@ module Flag
monochrome a 0 b Blue and
monochrome a b r White and
monochrome a r n Red)
and permut a (old a) 0 (n-1) }
and permut_sub a (old a) 0 (n-1) }
end
......
examples/programs/list_rev.mlw
View file @ 74cded5f
......@@ -9,25 +9,25 @@ module M
logic null : pointer
parameter value : ref (t pointer int)
parameter next : ref (t pointer pointer)
parameter value : ref (map pointer int)
parameter next : ref (map pointer pointer)
inductive is_list (next : t pointer pointer) (p : pointer) =
inductive is_list (next : map pointer pointer) (p : pointer) =
| is_list_null:
forall next : t pointer pointer, p : pointer.
forall next : map pointer pointer, p : pointer.
p = null -> is_list next p
| is_list_next:
forall next : t pointer pointer, p : pointer.
forall next : map pointer pointer, p : pointer.
p <> null -> is_list next (get next p) -> is_list next p
logic sep_list_list (next : t pointer pointer) (p1 p2 : pointer)
logic sep_list_list (next : map pointer pointer) (p1 p2 : pointer)
axiom sep_list_list_p_null:
forall next : t pointer pointer, p : pointer.
forall next : map pointer pointer, p : pointer.
sep_list_list next p null
axiom sep_list_list_null_p:
forall next : t pointer pointer, p : pointer.
forall next : map pointer pointer, p : pointer.
sep_list_list next null p
let list_rev (p : ref pointer) =
......
examples/programs/muller.mlw
View file @ 74cded5f
......@@ -5,22 +5,22 @@ module Muller
use import module stdlib.Refint
use import module stdlib.Array
type param = map int
logic pr (a : param) (n : int) = a[n] <> 0
type param = M.map int int
logic pr (a : param) (n : int) = M.get a n <> 0
clone import int.NumOfParam with type param = param, logic pr = pr
let compact (a : array int) =
let count = ref 0 in
for i = 0 to length a - 1 do
invariant { 0 <= count = num_of a 0 i <= i}
invariant { 0 <= count = num_of a.elts 0 i <= i}
if a[i] <> 0 then incr count
done;
let u = make !count 0 in
count := 0;
for i = 0 to length a - 1 do
invariant { 0 <= count = num_of a 0 i <= i and
length u = num_of a 0 (length a) }
if a[i] <> 0 then begin u[!count <- a[i]]; incr count end
invariant { 0 <= count = num_of a.elts 0 i <= i and
length u = num_of a.elts 0 (length a) }
if a[i] <> 0 then begin set u !count a[i]; incr count end
done
end
......
examples/programs/next_digit_sum.mlw
View file @ 74cded5f
......@@ -11,15 +11,11 @@ module M
use import int.Int
use import module stdlib.Ref
use array.ArrayLength as A
use import module stdlib.Array
use import int.MinMax
use import int.EuclideanDivision
use import int.Power
type array = A.t int int
logic (#) (a : array) (i : int) : int = A.get a i
logic sum_digits int : int
axiom Sum_digits_def : forall n : int. sum_digits n =
......@@ -27,52 +23,46 @@ module M
(* interp x i j is the integer X[j-1]...X[i] *)
logic interp array int int : int
logic interp (M.map int int) int int : int
axiom Interp_1 :
forall x : array, i j : int.
forall x : M.map int int, i j : int.
i >= j -> interp x i j = 0
axiom Interp_2 :
forall x : array, i j : int.
i < j -> interp x i j = x#i + 10 * interp x (i+1) j
forall x : M.map int int, i j : int.
i < j -> interp x i j = M.get x i + 10 * interp x (i+1) j
(* to allow provers to prove that an assignment does not change the
interpretation on the left (or on the right); requires induction *)
lemma Interp_eq:
forall x1 x2 : array, i j : int.
(forall k : int. i <= k < j -> x1#k = x2#k) -> interp x1 i j = interp x2 i j
forall x1 x2 : M.map int int, i j : int.
(forall k : int. i <= k < j -> M.get x1 k = M.get x2 k) ->
interp x1 i j = interp x2 i j
(* the sum of the elements of x[i..j[ *)
clone export sum.Sum with type container = array, logic f = A.get
(* logic sum_digits_a (x : array) (i j : int) : int = sum x i j *)
type map_int = M.map int int
clone export sum.Sum with type container = map_int, logic f = M.get
lemma Sum_is_sum_digits_interp:
forall x : array, i j : int.
forall x : M.map int int, i j : int.
sum x i j = sum_digits (interp x i j)
lemma Sum_digits_a_set_eq:
forall x : array, i j k v : int.
(k < i or k >= j) -> sum (A.set x k v) i j = sum x i j
forall x : array int, i j k v : int.
(k < i or k >= j) -> sum (M.set x.elts k v) i j = sum x.elts i j
(* interp9 X i j is the j-digit integer obtained by replacing the i least
significant digits in X by 9, i.e. X[j-1]...X[i]9...9 *)
logic interp9 (x : array) (i j : int) : int =
logic interp9 (x : M.map int int) (i j : int) : int =
power 10 i * (interp x i j + 1) - 1
lemma Interp9_step:
forall x : array, i j : int.
i < j -> interp9 (A.set x i 9) i j = interp9 x (i+1) j
let array_get (a : ref array) i =
{ 0 <= i < A.length a } A.get !a i { result = A.get a i }
let array_set (a : ref array) i v =
{ 0 <= i < A.length a } a := A.set !a i v { a = A.set (old a) i v }
forall x : M.map int int, i j : int.
i < j -> interp9 (M.set x i 9) i j = interp9 x (i+1) j
parameter x : ref (array)
parameter x : array int
(* the number of digits of X *)
logic n : int
......@@ -90,30 +80,30 @@ exception Success
(and termination, implicitely proved since we only have for loops) *)
let search_safety () =
{ A.length x = m }
{ length x = m }
label Init:
let s = ref 0 in
for i = 0 to m - 1 do (* could be n instead of m *)
s := !s + array_get x i
s := !s + get x i
done;
for d = 0 to m - 1 do
invariant { A.length x = m }
for c = array_get x d + 1 to 9 do
invariant { A.length x = m }
let delta = y - !s - c + array_get x d in
invariant { length x = m }
for c = get x d + 1 to 9 do
invariant { length x = m }
let delta = y - !s - c + get x d in
if 0 <= delta && delta <= 9 * d then begin
array_set x d c;
set x d c;
let k = div delta 9 in
for i = 0 to d - 1 do
invariant { A.length x = m }
if i < k then array_set x i 9
else if i = k then array_set x i (mod delta 9)
else array_set x i 0
invariant { length x = m }
if i < k then set x i 9
else if i = k then set x i (mod delta 9)
else set x i 0
done;
raise Success
end
done;
s := !s - array_get x d
s := !s - get x d
done
{ true } | Success -> { true }
......@@ -121,48 +111,48 @@ let search_safety () =
with digit sum y *)
(* x[0..m-1] is a well-formed integer i.e. has digits in 0..9 *)
logic is_integer (x : array) =
forall k : int. 0 <= k < m -> 0 <= x#k <= 9
logic is_integer (x : M.map int int) =
forall k : int. 0 <= k < m -> 0 <= M.get x k <= 9
let search () =
{ A.length x = m and is_integer x }
{ length x = m and is_integer x.elts }
label Init:
let s = ref 0 in
for i = 0 to m - 1 do (* could be n instead of m *)
invariant { s = sum x 0 i }
s := !s + array_get x i
invariant { s = sum x.elts 0 i }
s := !s + get x i
done;
assert { s = sum x 0 m };
assert { s = sum x.elts 0 m };
for d = 0 to m - 1 do
invariant {
x = at x Init and
s = sum x d m
s = sum x.elts d m
}
for c = array_get x d + 1 to 9 do
for c = get x d + 1 to 9 do
invariant { x = at x Init }
let delta = y - !s - c + array_get x d in
let delta = y - !s - c + get x d in
if 0 <= delta && delta <= 9 * d then begin
array_set x d c;
assert { sum x d m = y - delta };
set x d c;
assert { sum x.elts d m = y - delta };
let k = div delta 9 in
assert { k <= d };
for i = 0 to d - 1 do
invariant { A.length x = m and is_integer x and
sum x d m = y - delta and
sum x 0 i = if i <= k then 9*i else delta }
if i < k then array_set x i 9
else if i = k then array_set x i (mod delta 9)
else array_set x i 0
invariant { length x = m and is_integer x.elts and
sum x.elts d m = y - delta and
sum x.elts 0 i = if i <= k then 9*i else delta }
if i < k then set x i 9
else if i = k then set x i (mod delta 9)
else set x i 0
done;
(* assume { sum !x 0 d = delta }; *)
assert { sum x 0 d = delta };
assert { sum x.elts 0 d = delta };
raise Success
end
done;
s := !s - array_get x d
s := !s - get x d
done
{ true }
| Success -> { is_integer x and sum x 0 m = y }
| Success -> { is_integer x.elts and sum x.elts 0 m = y }
(* 3. Correctness, part 2: we now prove that, on success, x contains the
smallest integer > old(x) with digit sum y
......@@ -170,18 +160,18 @@ let search () =
4. Completeness: we always raise the Success exception *)
(* x1 > x2 since x1[d] > x2[d] and x1[d+1..m-1] = x2[d+1..m-1] *)
logic gt_digit (x1 x2 : array) (d : int) =
logic gt_digit (x1 x2 : M.map int int) (d : int) =
is_integer x1 and is_integer x2 and 0 <= d < m and
x1#d > x2#d and forall k : int. d < k < m -> x1#k = x2#k
M.get x1 d > M.get x2 d and forall k : int. d < k < m -> M.get x1 k = M.get x2 k
lemma Gt_digit_interp:
forall x1 x2 : array, d : int.
forall x1 x2 : M.map int int, d : int.
gt_digit x1 x2 d -> interp x1 0 m > interp x2 0 m
lemma Gt_digit_update:
forall x1 x2 : array, d i v : int.
forall x1 x2 : M.map int int, d i v : int.
gt_digit x1 x2 d -> 0 <= i < d -> 0 <= v <= 9 ->
gt_digit (A.set x1 i v) x2 d
gt_digit (M.set x1 i v) x2 d
(* the number of digits of a given integer *)
logic nb_digits int : int
......@@ -195,7 +185,7 @@ let search () =
(* the smallest integer with digit sum y is (y mod 9)9..9
with exactly floor(y/9) trailing 9s *)
logic smallest int : array
logic smallest int : M.map int int
logic smallest_size int : int
......@@ -209,7 +199,7 @@ let search () =
(* smallest(y) is an integer *)
axiom Smallest_def1:
forall y : int. y >= 0 ->
forall k : int. 0 <= k < smallest_size y -> 0 <= smallest y # k <= 9
forall k : int. 0 <= k < smallest_size y -> 0 <= M.get (smallest y) k <= 9
(* smallest(y) has digit sum y *)
axiom Smallest_def2:
......@@ -224,12 +214,12 @@ let search () =
lemma Smallest_shape_1:
forall y : int. y >= 0 -> mod y 9 = 0 ->
forall k : int. 0 <= k < smallest_size y -> smallest y # k = 9