Commit 2a4fe549 authored by MARCHE Claude's avatar MARCHE Claude

work in progress

parent 2e456272
......@@ -191,8 +191,8 @@ goods examples/bts
goods examples/tests
goods examples/tests-provers
goods examples/check-builtin
goods examples/logic
goods examples
goods examples/logic
goods examples/foveoos11-cm
goods examples/hoare_logic
goods examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps"
......
......@@ -272,6 +272,8 @@ Thi-Minh-Tuyen Nguyen, Asma Tafat, Piotr Trojanek.
\hline
\texttt{'L:} & \texttt{label L in} \\
\texttt{at !x 'L} & \texttt{!x at L} \\
\verb|\|\texttt{ x. t} & \texttt{fun x -> t} \\
\texttt{type t model ...} & \texttt{type t = private ... } \\
\hline
\end{tabular}
\end{center}
......
......@@ -10,13 +10,16 @@ module Bag
forall x: 'a. b1 x = b2 x
constant empty : bag 'a =
\ _. 0
fun _ -> 0
val empty () : bag 'a
ensures { result = empty }
function add (e: 'a) (b: bag 'a) : bag 'a =
\ x. if x = e then b x + 1 else b x
fun x -> if x = e then b x + 1 else b x
function remove (e: 'a) (b: bag 'a) : bag 'a =
\ x. if x = e then b x - 1 else b x
fun x -> if x = e then b x - 1 else b x
end
......@@ -25,7 +28,7 @@ module BagSpec
use import int.Int
use import Bag
type t 'a model {
type t 'a = private {
mutable size: int;
mutable contents: bag 'a;
}
......@@ -51,30 +54,34 @@ module ResizableArraySpec
use import int.Int
use import map.Map
type rarray 'a model { mutable length: int; mutable data: map int 'a }
type rarray 'a = private { mutable length: int; 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 length (r: rarray ~'a) : int
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 length (r: rarray 'a) : int
ensures { result = r.length }
*)
val make (len: int) (dummy: ~'a) : rarray 'a
val make (len: int) (dummy: 'a) : rarray 'a
requires { 0 <= len }
ensures { result.length = len }
ensures { result.data = Map.const dummy }
val ([]) (r: rarray ~'a) (i: int) : 'a
val ([]) (r: rarray 'a) (i: int) : 'a
requires { 0 <= i < r.length }
ensures { result = r[i] }
val ([]<-) (r: rarray ~'a) (i: int) (v: 'a) : unit
val ([]<-) (r: rarray 'a) (i: int) (v: 'a) : unit
requires { 0 <= i < r.length }
writes { r.data }
ensures { r = (old r)[i <- v] }
val resize (r: rarray ~'a) (len: int) : unit
val resize (r: rarray 'a) (len: int) : unit
requires { 0 <= len }
writes { r.length, r.data }
ensures { r.length = len }
......@@ -93,24 +100,24 @@ module BagImpl
use null.Null
function numof (r: rarray (Null.t 'a)) (x: 'a) (l u: int) : int =
NumOf.numof (\i. (Map.get r.R.data i).Null.v = Null.Value x) l u
NumOf.numof (fun i -> (Map.get r.R.data i).Null.v = Null.Value x) l u
type t 'a = {
mutable size: int;
data: rarray (Null.t 'a);
mutable ghost contents: bag 'a;
}
invariant { 0 <= self.size = self.data.length }
invariant { forall i: int. 0 <= i < self.size ->
not (Null.is_null self.data[i]) }
invariant { forall x: 'a. self.contents x = numof self.data x 0 self.size }
invariant { 0 <= size = data.length }
invariant { forall i: int. 0 <= i < size ->
not (Null.is_null data[i]) }
invariant { forall x: 'a. contents x = numof data x 0 size }
let create () : t 'a
ensures { result.size = 0 }
ensures { result.contents == Bag.empty }
=
let null = Null.create_null () : Null.t 'a in
{ size = 0; data = make 0 null; contents = Bag.empty }
{ size = 0; data = make 0 null; contents = Bag.empty () }
let clear (t: t 'a) : unit
ensures { t.size = 0 }
......@@ -118,7 +125,7 @@ module BagImpl
=
resize t.data 0;
t.size <- 0;
t.contents <- Bag.empty
t.contents <- Bag.empty ()
let add (t: t 'a) (x: 'a) : unit
ensures { t.size = old t.size + 1 }
......
......@@ -273,7 +273,7 @@ module Solver
let v = g[s + offsets[off]] in
if 1 <= v && v <= 9 then
begin
if b[v] = True then raise Invalid;
if b[v] then raise Invalid;
b[v] <- True
end
done
......@@ -422,13 +422,13 @@ this is true but with 2 different possible reasons:
end
else
begin
'L:
label L in
for k = 1 to 9 do
invariant { grid_eq (at g 'L).elts (Map.set g.elts i 0) }
invariant { grid_eq (g at L).elts (Map.set g.elts i 0) }
invariant { full_up_to g.elts i }
invariant { (* for completeness *)
forall k'. 1 <= k' < k ->
let g' = Map.set (at g 'L).elts i k' in
let g' = Map.set (g at L).elts i k' in
forall h : grid. included g' h /\ full h -> not (valid s h) }
g[i] <- k;
try
......@@ -436,7 +436,7 @@ this is true but with 2 different possible reasons:
check_valid_chunk g i s.row_start s.row_offsets;
check_valid_chunk g i s.square_start s.square_offsets;
(* the hard part: see lemma valid_up_to_change *)
assert { let grid' = Map.set (at g 'L).elts i k in
assert { let grid' = Map.set (g at L).elts i k in
grid_eq grid' g.elts &&
valid_chunk grid' i s.column_start s.column_offsets &&
valid_chunk grid' i s.row_start s.row_offsets &&
......@@ -446,17 +446,17 @@ this is true but with 2 different possible reasons:
solve_aux s g (i + 1)
with Invalid ->
assert { (* for completeness *)
not (valid s (Map.set (at g 'L).elts i k)) };
not (valid s (Map.set (g at L).elts i k)) };
assert { (* for completeness *)
let g' = Map.set (at g 'L).elts i k in
let g' = Map.set (g at L).elts i k in
forall h : grid. included g' h /\ full h -> not (valid s h) }
end
done;
g[i] <- 0;
assert { (* for completeness *)
forall h:grid. included (at g 'L).elts h /\ full h ->
forall h:grid. included (g at L).elts h /\ full h ->
let k' = Map.get h i in
let g' = Map.set (at g 'L).elts i k' in
let g' = Map.set (g at L).elts i k' in
included g' h }
end
......@@ -531,13 +531,13 @@ module RandomSolver
end
else
begin
'L:
label L in
for k = 1 to 9 do
invariant { grid_eq (at g 'L).elts (Map.set g.elts j 0) }
invariant { grid_eq (g at L).elts (Map.set g.elts j 0) }
invariant { full_up_to g.elts i } (* TODO i -> j *)
invariant { (* for completeness *)
forall k'. 1 <= k' < k ->
let g' = Map.set (at g 'L).elts i k' in (* TODO i -> j *)
let g' = Map.set (g at L).elts i k' in (* TODO i -> j *)
forall h : grid. included g' h /\ full h -> not (valid s h) }
g[j] <- k;
try
......@@ -546,7 +546,7 @@ module RandomSolver
check_valid_chunk g j s.square_start s.square_offsets;
(* the hard part: see lemma valid_up_to_change *)
(* TODO i -> j *)
assert { let grid' = Map.set (at g 'L).elts i k in
assert { let grid' = Map.set (g at L).elts i k in
grid_eq grid' g.elts &&
valid_chunk grid' i s.column_start s.column_offsets &&
valid_chunk grid' i s.row_start s.row_offsets &&
......@@ -556,17 +556,17 @@ module RandomSolver
solve_aux s randoffset g (i + 1)
with Invalid ->
assert { (* for completeness *)
not (valid s (Map.set (at g 'L).elts i k)) };
not (valid s (Map.set (g at L).elts i k)) };
assert { (* for completeness *)
let g' = Map.set (at g 'L).elts i k in
let g' = Map.set (g at L).elts i k in
forall h : grid. included g' h /\ full h -> not (valid s h) }
end
done;
g[j] <- 0;
assert { (* for completeness *)
forall h:grid. included (at g 'L).elts h /\ full h ->
forall h:grid. included (g at L).elts h /\ full h ->
let k' = Map.get h i in
let g' = Map.set (at g 'L).elts i k' in
let g' = Map.set (g at L).elts i k' in
included g' h }
end
......@@ -612,8 +612,8 @@ module Test
use import TheClassicalSudokuGrid
use import Solver
use array.Array
use import map.Map
use import array.Array
(** Solving the empty grid: easy, yet not trivial *)
let test0 ()
......@@ -644,28 +644,39 @@ module Test
8 0 0 0 0 1 0 0 5
0 0 0 0 0 0 0 7 6
*)
constant solvable : grid =
(const 0)
[0<-2][2<-9][7<-1]
[13<-6]
[19<-5][20<-3][21<-8][23<-2][24<-7]
[27<-3]
[40<-7][41<-5][44<-3]
[46<-4][47<-1][48<-2][50<-8][51<-9]
[56<-4][58<-9][61<-2]
[63<-8][68<-1][71<-5]
[79<-7][80<-6]
lemma valid_values_solvable: valid_values solvable
let test1 ()
raises { NoSolution -> true }
= let a = Array.make 81 0 in
for i = 0 to 80 do
invariant { valid_values a.Array.elts }
Array.([]<-) a i (Map.get solvable i)
done;
a[0] <- 2;
a[2] <- 9;
a[7] <- 1;
a[13] <- 6;
a[19] <- 5;
a[20] <- 3;
a[21] <- 8;
a[23] <- 2;
a[24] <- 7;
a[27] <- 3;
a[40] <- 7;
a[41] <- 5;
a[44] <- 3;
a[46] <- 4;
a[47] <- 1;
a[48] <- 2;
a[50] <- 8;
a[51] <- 9;
a[56] <- 4;
a[58] <- 9;
a[61] <- 2;
a[63] <- 8;
a[68] <- 1;
a[71] <- 5;
a[79] <- 7;
a[80] <- 6;
assert { valid_values a.Array.elts };
solve (classical_sudoku()) a
(* the solution:
2, 6, 9, 3, 5, 7, 8, 1, 4,
......
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