Commit 901711d7 authored by MARCHE Claude's avatar MARCHE Claude

build maze with theories and modules

parent 76d04eaa
module M
theory UnionFind
use import int.Int
use import module stdlib.Ref
type uf
......@@ -10,112 +10,150 @@ module M
logic num uf : int
axiom Repr_function_1:
forall u:uf, x:int.
forall u:uf, x:int.
0 <= x < size u -> exists y:int. 0 <= y < size u and repr u x y
axiom Repr_function_2:
forall u:uf, x y z:int.
forall u:uf, x y z:int.
0 <= x < size u -> repr u x y -> repr u x z -> y = z
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
parameter create :
n:int ->
{ 0 <= n }
ref uf
end
module UnionFind_sig
use import int.Int
use import module stdlib.Ref
use export UnionFind
parameter create :
n:int ->
{ 0 <= n }
ref uf
{ num result = n and size result = n and
forall x:int. 0 <= x < n -> repr result x x }
parameter find :
u:ref uf -> x:int ->
{ 0 <= x < size u }
int writes u
{ repr u x result and
size u = size (old u) and num u = num (old u) and
same_reprs u (old u) }
parameter find :
u:ref uf -> x:int ->
{ 0 <= x < size u }
int writes u
{ repr u x result and
size u = size (old u) and num u = num (old u) and
same_reprs u (old u) }
parameter union :
u:ref uf -> a:int -> b:int ->
parameter union :
u:ref uf -> a:int -> b:int ->
{ 0 <= a < size u and 0 <= b < size u and not same u a b }
unit writes u
{ same u a b and
size u = size (old u) and num u = num (old u) - 1 and
forall x y:int. 0 <= x < size u -> 0 <= y < size u ->
size u = size (old u) and num u = num (old u) - 1 and
forall x y:int. 0 <= x < size u -> 0 <= y < size u ->
same u x y <->
same (old u) x y or
same (old u) x a and same (old u) b y or
same (old u) x b and same (old u) a y }
parameter get_num_classes :
parameter get_num_classes :
u:ref uf -> {} int reads u { result = num u }
parameter rand : s:int -> { 0 < s } int { 0 <= result < s }
lemma Ineq1 :
forall n x y:int. 0 <= n -> 0 <= x < n -> 0 <= y < n -> 0 <= x*n+y < n*n
end
theory Graph
type vertex
type graph
(*clone import graph.Path with type graph = graph, type vertex = int*)
logic path graph int int
axiom Path_refl : forall g:graph, x:int. path g x x
axiom Path_sym : forall g:graph, x y:int. path g x y -> path g y x
axiom Path_trans:
forall g:graph, x y z:int. path g x y -> path g y z -> path g x z
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_trans:
forall g:graph, x y z:vertex. path g x y -> path g y z -> path g x z
logic select (d:int) (x y:'a) : 'a = if d = 0 then x else y
end
parameter graph : ref graph
theory Graph_int
parameter num_edges : ref int
clone export Graph with type vertex = int
parameter add_edge :
a:int -> b:int ->
{ not path graph a b }
unit writes num_edges graph
end
module Graph_sig
use import int.Int
use import module stdlib.Ref
clone export Graph with type vertex = int
(* use export Graph *)
(* use export Graph_int*)
parameter graph : ref graph
parameter num_edges : ref int
parameter add_edge : a:int -> b:int ->
{ not path graph a b }
unit writes num_edges graph
{ num_edges = old num_edges + 1 and
(forall x y:int.
(forall x y:int.
path graph x y <->
path (old graph) x y or
path (old graph) x y or
path (old graph) x a and path (old graph) b y or
path (old graph) x b and path (old graph) a y)
path (old graph) x b and path (old graph) a y)
}
let add_edge_and_union u (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.
0 <= x < size u -> 0 <= y < size u ->
same u x y <-> path graph x y
}
add_edge a b;
union u a b
{ num_edges = old num_edges + 1 and
same u a b and
size u = size (old u) and num u = num (old u) - 1 and
(forall x y:int.
0 <= x < size u -> 0 <= y < size u ->
same u x y <-> path graph x y)
}
end
module BuildMaze
use import int.Int
use import module stdlib.Ref
use import module UnionFind_sig
use import module Graph_sig
parameter rand : s:int -> { 0 < s } int { 0 <= result < s }
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) =
{ 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.
0 <= x < size u -> 0 <= y < size u ->
same u x y <-> path graph x y
}
add_edge a b;
union u a b
{ num_edges = old num_edges + 1 and
same u a b and
size u = size (old u) and num u = num (old u) - 1 and
(forall x y:int.
0 <= x < size u -> 0 <= y < size u ->
same u x y <-> path graph x y)
}
let build_maze (n:int) =
{ 1 <= n and
num_edges = 0 and
forall x y:int. x=y <-> path graph x y
{ 1 <= n and
num_edges = 0 and
forall x y:int. x=y <-> path graph x y
}
let u = create (n*n) in
assert { forall x y:int. 0 <= x < n*n -> 0 <= y < n*n ->
same u x y -> (repr u x y && repr u x x && x = y) };
while get_num_classes u > 1 do
invariant
invariant
{ 1 <= num u and num u + num_edges = size u = n*n and
forall x y:int. 0 <= x < n*n -> 0 <= y < n*n ->
(same u x y <-> path graph x y)
......@@ -135,13 +173,13 @@ let build_maze (n:int) =
end
done
{ num_edges = n*n-1 and
forall x y:int. 0 <= x < n*n -> 0 <= y < n*n ->
forall x y:int. 0 <= x < n*n -> 0 <= y < n*n ->
path graph x y }
end
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/vacid_0_build_maze"
End:
End:
*)
......@@ -165,9 +165,11 @@ let create_module n =
in
(* pervasives *)
let m = add_esymbol ls_Exit m in
(*
let m = add_mtsymbol mt_ghost m in
let m = add_psymbol ps_ghost m in
let m = add_psymbol ps_unghost m in
*)
m
(** Modules *)
......
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