Commit 5c138ad7 by Andrei Paskevich

### higher-order application syntax

parent 9f30f6bc
 ... ... @@ -6,9 +6,9 @@ parameter r : int ref parameter f1 : y:int -> {} unit writes r { q1(!r, old(!r), y) } {} unit writes r { q1 (!r) (old (!r)) y } let g1 () = {} f1 !r { q1(!r, old(!r), old(!r)) } let g1 () = {} f1 !r { q1 (!r) (old (!r)) (old (!r)) } { logic foo(int) : int ... ... @@ -16,12 +16,12 @@ let g1 () = {} f1 !r { q1(!r, old(!r), old(!r)) } } parameter f : t:int ref -> x:int -> {} unit reads t writes t { q(!t, old(!t), x) } {} unit reads t writes t { q (!t) (old (!t)) x } let g (t:int ref) = {} f t (foo !t) { q(!t, old(!t), foo(old(!t))) } { q (!t) (old (!t)) (foo (old (!t))) } (* ... ...
 parameter x : int ref parameter f : unit -> { } unit writes x { !x = 1 - old(!x) } parameter f : unit -> { } unit writes x { !x = 1 - old (!x) } let p () = begin ... ... @@ -9,7 +9,7 @@ let p () = let t = () in (); (f ()); (f ()); assert { !x = at(!x, Init) }; assert { !x = at (!x) Init }; () end ... ...
 ... ... @@ -8,6 +8,6 @@ type t2 = t5 logic f(x : t1, y : t2) : t5 logic g(x : t1) : t5 = f(x,x) logic g(x : t1) : t5 = f x x end \ No newline at end of file end
 ... ... @@ -2,6 +2,6 @@ theory Test type t logic f(t,t) : t clone algebra.AC with type t = t, logic op = f goal G1 : forall x,y : t. f(x,y) = f(y,x) goal G2 : forall x,y,z : t. f(f(x,y),z) = f(x,f(y,z)) end \ No newline at end of file goal G1 : forall x,y : t. f x y = f y x goal G2 : forall x,y,z : t. f (f x y) z = f x (f y z) end
 theory Test use import int.EuclideanDivision goal G1 : mod(10,3) = 1 goal G2 : div(10,3) = 3 end \ No newline at end of file goal G1 : mod 10 3 = 1 goal G2 : div 10 3 = 3 end
 ... ... @@ -31,7 +31,7 @@ logic invariant(x:int, y:int, e:int) = e = 2 * (x + 1) * y2 - (2 * y + 1) * x2 and 2 * (y2 - x2) <= e <= 2 * y2 lemma Invariant_is_ok : forall x,y,e:int. invariant(x,y,e) -> best(x,y) lemma Invariant_is_ok : forall x,y,e:int. invariant x y e -> best x y } let bresenham () = ... ... @@ -39,10 +39,10 @@ let bresenham () = let y = ref 0 in let e = ref (2 * y2 - x2) in while !x <= x2 do invariant {0 <= !x and !x <= x2 + 1 and invariant(!x, !y, !e) } invariant {0 <= !x and !x <= x2 + 1 and invariant !x !y !e } variant { x2 + 1 - !x } (* here we would plot (x, y) *) assert { best(!x, !y) }; assert { best !x !y }; if !e < 0 then e := !e + 2 * y2 else begin ... ...
 ... ... @@ -9,13 +9,13 @@ parameter set_has_next : s:'a S.t ref -> {} bool reads s { if result=True then S.is_empty(!s) else not S.is_empty(!s) } { if result=True then S.is_empty !s else not S.is_empty !s } parameter set_next : s:'a S.t ref -> { not S.is_empty(!s) } { not S.is_empty !s } 'a writes s { S.mem(result, old(!s)) and !s = S.remove(result, old(!s)) } { S.mem result (old !s) and !s = S.remove result (old !s) } { (* the graph *) ... ... @@ -27,11 +27,11 @@ logic v : vertex S.t logic g_succ(vertex) : vertex S.t axiom G_succ_sound : forall x:vertex. S.subset(g_succ(x), v) forall x:vertex. S.subset (g_succ x) v logic weight(vertex, vertex) : int (* edge weight, if there is an edge *) axiom Weight_nonneg : forall x,y:vertex. weight(x,y) >= 0 axiom Weight_nonneg : forall x,y:vertex. weight x y >= 0 } parameter eq_vertex : ... ... @@ -42,7 +42,7 @@ parameter eq_vertex : parameter visited : vertex S.t ref parameter visited_add : x:vertex -> {} unit writes visited { !visited = S.add(x, old(!visited)) } x:vertex -> {} unit writes visited { !visited = S.add x (old !visited) } (* current distances *) ... ... @@ -56,153 +56,153 @@ parameter q_is_empty : unit -> {} bool reads q { if result=True then S.is_empty(!q) else not S.is_empty(!q) } { if result=True then S.is_empty !q else not S.is_empty !q } parameter init : src:vertex -> {} unit writes visited, q, d { S.is_empty(!visited) and !q = S.add(src, S.empty) and !d = M.store(old(!d), src, 0) } { S.is_empty !visited and !q = S.add src S.empty and !d = M.store (old !d) src 0 } parameter relax : u:vertex -> v:vertex -> {} unit reads visited writes d,q { (S.mem(v, !visited) and !q = old(!q) and !d = old(!d)) { (S.mem v !visited and !q = old !q and !d = old !d) or (S.mem(v,!q) and M.select(!d,u) + weight(u,v) >= M.select(!d,v) and !q = old(!q) and !d = old(!d)) (S.mem v !q and M.select !d u + weight u v >= M.select !d v and !q = old !q and !d = old !d) or (S.mem(v,!q) and M.select(!d,u) + weight(u,v) < M.select(!d,v) and !q = old(!q) and !d = M.store(old(!d), v, M.select(!d,u) + weight(u,v))) (S.mem v !q and M.select !d u + weight u v < M.select !d v and !q = old !q and !d = M.store (old !d) v (M.select !d u + weight u v)) or (not S.mem(v, !visited) and not S.mem(v,!q) and !q = S.add(v,old(!q)) and !d = M.store(old(!d), v, M.select(!d,u) + weight(u,v))) } (not S.mem v !visited and not S.mem v !q and !q = S.add v (old !q) and !d = M.store (old !d) v (M.select !d u + weight u v)) } { logic min(m:vertex, q:vertex S.t, d:(vertex, int) M.t) = S.mem(m, q) and forall x:vertex. S.mem(x, q) -> M.select(d,x) <= M.select(d,m) S.mem m q and forall x:vertex. S.mem x q -> M.select d x <= M.select d m } parameter q_extract_min : unit -> { not S.is_empty(!q) } { not S.is_empty !q } vertex reads d writes q { min(result, old(!q), !d) and !q = S.remove(result, old(!q)) } { min result (old !q) !d and !q = S.remove result (old !q) } (* paths and shortest paths path(x,y,d) = path x y d = there is a path from x to y of length d shortest_path(x,y,d) = shortest_path x y d = there is a path from x to y of length d, and no shorter path *) { inductive path(vertex, vertex, int) = inductive path(vertex,vertex,int) = | Path_nil : forall x:vertex. path(x, x, 0) forall x:vertex. path x x 0 | Path_cons : forall x,y,z:vertex. forall d:int. path(x, y, d) -> S.mem(z, g_succ(y)) -> path(x, z, d+weight(y,z)) path x y d -> S.mem z (g_succ y) -> path x z (d+weight y z) lemma Length_nonneg : forall x,y:vertex. forall d:int. path(x,y,d) -> d >= 0 lemma Length_nonneg : forall x,y:vertex. forall d:int. path x y d -> d >= 0 logic shortest_path(x:vertex, y:vertex, d:int) = path(x,y,d) and forall d':int. path(x,y,d') -> d <= d' path x y d and forall d':int. path x y d' -> d <= d' lemma Path_inversion : forall src,v:vertex. forall d:int. path(src,v,d) -> forall src,v:vertex. forall d:int. path src v d -> (v = src and d = 0) or (exists v':vertex. path(src,v',d - weight(v',v)) and S.mem(v, g_succ(v'))) (exists v':vertex. path src v' (d - weight v' v) and S.mem v (g_succ v')) lemma Path_shortest_path : forall src,v:vertex. forall d:int. path(src,v,d) -> exists d':int. shortest_path(src,v,d') and d' <= d forall src,v:vertex. forall d:int. path src v d -> exists d':int. shortest_path src v d' and d' <= d (* lemmas (those requiring induction) *) lemma Main_lemma : forall src,v:vertex. forall d:int. path(src,v,d) -> not shortest_path(src,v,d) -> path src v d -> not shortest_path src v d -> exists v':vertex. exists d':int. shortest_path(src,v',d') and S.mem(v,g_succ(v')) and d' + weight(v',v) < d shortest_path src v' d' and S.mem v (g_succ v') and d' + weight v' v < d lemma Completeness_lemma : forall s:vertex S.t. 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)) -> S.mem v s -> forall w:vertex. S.mem w (g_succ v) -> S.mem w s) -> (* and if s contains src *) S.mem(src, s) -> S.mem src s -> (* then any vertex reachable from s is also in s *) path(src, dst, d) -> S.mem(dst, s) path src dst d -> S.mem dst s (* definitions used in loop invariants *) logic inv_src(src:vertex, s:vertex S.t, q:vertex S.t) = S.mem(src,s) or S.mem(src,q) S.mem src s or S.mem src q logic inv(src:vertex, s:vertex S.t, q:vertex S.t, d:(vertex,int) M.t) = inv_src(src, s, q) inv_src src s q (* S,Q are contained in V *) and S.subset(s,v) and S.subset(q,v) and S.subset s v and S.subset q v (* S and Q are disjoint *) and (forall v:vertex. S.mem(v,q) -> S.mem(v,s) -> false) (forall v:vertex. S.mem v q -> S.mem v s -> false) (* we already found the shortest paths for vertices in S *) and (forall v:vertex. S.mem(v,s) -> shortest_path(src,v,M.select(d,v))) (forall v:vertex. S.mem v s -> shortest_path src v (M.select d v)) (* there are paths for vertices in Q *) and (forall v:vertex. S.mem(v,q) -> path(src,v,M.select(d,v))) (forall v:vertex. S.mem v q -> path src v (M.select d v)) (* vertices at distance < min(Q) are already in S *) and (forall m:vertex. min(m,q,d) -> forall x:vertex. forall dx:int. shortest_path(src,x,dx) -> dx < M.select(d,m) -> S.mem(x,s)) (forall m:vertex. min m q d -> forall x:vertex. forall dx:int. shortest_path src x dx -> dx < M.select d m -> S.mem x s) logic inv_succ(src:vertex, s:vertex S.t, q: vertex S.t) = (* 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)) (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:vertex S.t, q: vertex S.t, u:vertex, su:vertex S.t) = (* 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) -> forall y:vertex. S.mem(y,g_succ(x)) -> (x<>u or (x=u and not S.mem(y,su))) -> S.mem(y, s) or S.mem(y, q)) (forall x:vertex. S.mem x s -> forall y:vertex. S.mem y (g_succ x) -> (x<>u or (x=u and not S.mem y su)) -> S.mem y s or S.mem y q) } (* code *) let shortest_path_code (src:vertex) (dst:vertex) = { S.mem(src,v) and S.mem(dst,v) } { S.mem src v and S.mem dst v } init src; while not (q_is_empty ()) do invariant { inv(src, !visited, !q, !d) and inv_succ(src, !visited, !q) } variant { S.cardinal(v) - S.cardinal(!visited) } invariant { inv src !visited !q !d and inv_succ src !visited !q } variant { S.cardinal v - S.cardinal !visited } let u = q_extract_min () in assert { shortest_path(src, u, M.select(!d,u)) }; assert { shortest_path src u (M.select !d u) }; visited_add u; let su = ref (g_succ u) in while not (set_has_next su) do invariant { S.subset(!su, g_succ(u)) and inv(src, !visited, !q, !d) and inv_succ2(src, !visited, !q, u, !su) } variant { S.cardinal(!su) } { S.subset !su (g_succ u) and inv src !visited !q !d and inv_succ2 src !visited !q u !su } variant { S.cardinal !su } let v = set_next su in relax u v done done { (forall v:vertex. S.mem(v, !visited) -> shortest_path(src, v, M.select(!d,v))) S.mem v !visited -> shortest_path src v (M.select !d v)) and (forall v:vertex. not S.mem(v, !visited) -> forall dv:int. not path(src, v, dv)) } not S.mem v !visited -> forall dv:int. not path src v dv) } (* Local Variables: ... ...
 ... ... @@ -3,15 +3,15 @@ type uf logic repr(uf, int) : int logic size(uf) : int logic repr (uf,int): int logic size (uf) : int logic num (uf) : int logic same(u:uf, x:int, y:int) = repr(u, x) = repr(u, y) logic same(u:uf, x:int, y:int) = repr u x = repr u y axiom OneClass : forall u:uf. num(u) = 1 -> forall x,y:int. 0 <= x < size(u) -> 0 <= y < size(u) -> same(u, x, y) forall u:uf. num u = 1 -> forall x,y:int. 0 <= x < size u -> 0 <= y < size u -> same u x y } ... ... @@ -19,31 +19,31 @@ parameter create : n:int -> { 0 <= n } uf ref { num(!result) = n and size(!result) = n and forall x:int. 0 <= x < n -> repr(!result, x) = x } { num !result = n and size !result = n and forall x:int. 0 <= x < n -> repr !result x = x } parameter find : u:uf ref -> x:int -> { 0 <= x < size(!u) } { 0 <= x < size !u } int writes u { result = repr(!u, x) and size(!u) = size(old(!u)) and num(!u) = num(old(!u)) and forall x:int. 0 <= x < size(!u) -> repr(!u, x) = repr(old(!u), x) } { result = repr !u x and size !u = size (old !u) and num !u = num (old !u) and forall x:int. 0 <= x < size !u -> repr !u x = repr (old !u) x } parameter union : u:uf ref -> a:int -> b:int -> { 0 <= a < size(!u) and 0 <= b < size(!u) and not same(!u, a, b) } { 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) -> 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) } { 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 <-> 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 : u:uf ref -> {} int reads u { result = num(!u) } u:uf ref -> {} int reads u { result = num !u } parameter rand : s:int -> {} int { 0 <= result < s } ... ... @@ -56,12 +56,12 @@ parameter rand : s:int -> {} int { 0 <= result < s } type graph (*clone import graph.Path with type graph = graph, type vertex = int*) logic path(graph, int, 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_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) forall g:graph, x,y,z:int. path g x y -> path g y z -> path g x z logic select(d:int, x:'a, y:'a) : 'a = if d = 0 then x else y } ... ... @@ -72,44 +72,44 @@ parameter num_edges : int ref parameter add_edge : a:int -> b:int -> { not path(!graph, a, b) } { not path !graph a b } unit writes num_edges, graph { !num_edges = old(!num_edges) + 1 and { !num_edges = old !num_edges + 1 and (forall x,y:int. path(!graph, x, y) <-> 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 !graph x y <-> 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) } let add_edge_and_union (u:uf ref) (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 { 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) 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 { !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)) 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 -> not path(!graph, x, y) forall x,y:int. x<>y -> not path !graph x y } let u = create (n*n) in while get_num_classes u > 1 do invariant { 1 <= num(!u) and num(!u) + !num_edges = size(!u) = n*n and { 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) same !u x y <-> path !graph x y } let x = rand n in let y = rand n in ... ... @@ -127,7 +127,7 @@ let build_maze (n:int) = done { !num_edges = n*n-1 and forall x,y:int. 0 <= x < n*n -> 0 <= y < n*n -> path(!graph, x, y) } path !graph x y } (* Local Variables: ... ...
 ... ... @@ -31,7 +31,7 @@ back +-+-+-+-------------------+ type 'a array = 'a A.t logic (#)(a : 'a array, i : int) : 'a = A.select(a, i) logic (#)(a : 'a array, i : int) : 'a = A.select a i type sparse_array = elt array * int array * int array * int (*sz*) * int (*n*) ... ... @@ -47,8 +47,8 @@ back +-+-+-+-------------------+ 0 <= idx#i < n and back#(idx#i) = i logic model(a : sparse_array, i : int) : elt = if is_elt(a, i) then sa_val(a)#i if is_elt a i then (sa_val a)#i else default ... ... @@ -73,18 +73,18 @@ back +-+-+-+-------------------+ axiom Dirichlet : forall n : int. forall a : int array. permutation(n, a) -> permutation n a -> (forall i : int. 0 <= i < n -> 0 <= dirichlet(n,a,i) < n and a # dirichlet(n,a,i) = i) 0 <= dirichlet n a i < n and a # dirichlet n a i = i) lemma Inter6 : forall a : sparse_array . invariant(a) -> forall a : sparse_array . invariant a -> let (val, idx, back, sz, n) = a in n = sz -> permutation(sz, back) and permutation sz back and forall i : int. 0 <= i < sz -> idx#i = dirichlet(sz,back,i) and is_elt(a,i) idx#i = dirichlet sz back i and is_elt a i } ... ... @@ -93,23 +93,23 @@ parameter create : sz:int -> { 0 <= sz <= maxlen } sparse_array ref { sa_sz(!result) = sz and forall i:int. model(!result, i) = default } { sa_sz !result = sz and forall i:int. model !result i = default } *) (* BUG parameter malloc : n:int -> {} 'a array { A.length(result) = n } parameter malloc : n:int -> {} 'a array { A.length result = n } *) parameter malloc_elt : n:int -> {} elt array { A.length(result) = n } parameter malloc_int : n:int -> {} int array { A.length(result) = n } parameter malloc_elt : n:int -> {} elt array { A.length result = n } parameter malloc_int : n:int -> {} int array { A.length result = n } let create sz = { 0 <= sz <= maxlen } ref ((malloc_elt sz, malloc_int sz, malloc_int sz, sz, 0) : sparse_array) { invariant(!result) and sa_sz(!result) = sz and forall i:int. model(!result, i) = default } { invariant !result and sa_sz !result = sz and forall i:int. model !result i = default } let test a i = { 0 <= i < sa_sz(!a) } { 0 <= i < sa_sz !a } let idx = sa_idx !a in let back = sa_back !a in let n = sa_n !a in ... ... @@ -120,36 +120,36 @@ let test a i = False else False { result=True <-> is_elt(!a, i) } { result=True <-> is_elt !a i } (* parameter get : a:sparse_array ref -> i:int -> { 0 <= i < sa_sz(!a) } { 0 <= i < sa_sz !a } elt reads a { result = model(!a, i) } { result = model !a i } *) let get a i = { 0 <= i < sa_sz(!a) and invariant(!a) } { 0 <= i < sa_sz !a and invariant !a } let val = sa_val !a in if test a i then A.select val i else default { result = model(!a, i) } { result = model !a i } (* parameter set : a:sparse_array ref -> i:int -> v:elt -> { 0 <= i < sa_sz(!a) and invariant(!a) } { 0 <= i < sa_sz !a and invariant !a } unit writes a { invariant(!a) and sa_sz(!a) = sa_sz(old(!a)) and model(!a, i) = v and forall j:int. j <> i -> model(!a, j) = model(old(!a), j) } { invariant !a and sa_sz !a = sa_sz (old !a) and model !a i = v and forall j:int. j <> i -> model !a j = model (old !a) j } *) let set a i v = { 0 <= i < sa_sz(!a) and invariant(!a) } { 0 <= i < sa_sz !a and invariant !a } let val = sa_val !a in let idx = sa_idx !a in let back = sa_back !a in ... ... @@ -164,10 +164,10 @@ let set a i v = let back = A.store back n i in a := (val, idx, back, sz, n+1) end { invariant(!a) and sa_sz(!a) = sa_sz(old(!a)) and model(!a, i) = v and forall j:int. j <> i -> model(!a, j) = model(old(!a), j) } { invariant !a and sa_sz !a = sa_sz (old !a) and model !a i = v and forall j:int. j <> i -> model !a j = model (old !a) j } let harness () = let a = create 10 in ... ...
 ... ... @@ -5,7 +5,7 @@ type 'a array = 'a A.t logic (#)(a : 'a array, i : int) : 'a = A.select(a, i) logic (#)(a : 'a array, i : int) : 'a = A.select a i type uf = (* link: *) int array * (* dist: *) int array * (* distance to representative *) ... ... @@ -26,18 +26,18 @@ logic repr(u:uf, x:int) : int = let l = link(u) in let y = l#x in if y = x then y else repr(u, y) if y = x then y else repr u y logic same(u:uf, x:int, y:int) = repr(u, x) = repr(u, y) logic same(u:uf, x:int, y:int) = repr u x = repr u y axiom OneClass : forall u:uf. num(u) = 1 -> forall x,y:int. 0 <= x < size(u) -> 0 <= y < size(u) -> same(u, x, y) 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:uf ref) = {} num !u { result = num(!u) } {} num !u { result = num !u } let create (n:int) = { 0 <= n } ... ... @@ -52,63 +52,63 @@ let create (n:int) = i := !i + 1 done; ref ((!l, A.const_length 0 n, n, n)) { inv(!result) and num(!result) = n and size(!result) = n and forall x:int. 0 <= x < n -> repr(!result, x) = x } { inv !result and num !result = n and size !result = n and forall x:int. 0 <= x < n -> repr !result x = x } let find (u:uf ref) (x:int) = { inv(!u) and 0 <= x < size(!u) } { inv !u and 0 <= x < size !u } let l = link !u in let y = ref x in while A.select l !y <> !y do invariant { 0 <= !y < size(!u) and same(!u, x, !y) } invariant { 0 <= !y < size !u and same !u x !y } variant { dist(!u) # !y } y := A.select l !y done; !y { inv(!u) and result = repr(!u, x) and size(!u) = size(old(!u)) and num(!u) = num(old(!u)) and forall x:int. 0 <= x < size(!u) -> repr(!u, x) = repr(old(!u), x) } { inv !u and result = repr !u x and size !u = size (old !u) and num !u = num (old !u) and forall x:int. 0 <= x < size !u -> repr !u x = repr (old !u) x } parameter ghost_find : u:uf ref -> x:int -> { inv(!u) and 0 <= x < size(!u) } { inv !u and 0 <= x < size !u } int reads u { result = repr(!u, x) } { result = repr !u x } let increment (u : uf ref) (r : int) = { inv(!u) and 0 <= r < size(!u) } { inv !u and 0 <= r < size !u } let i = ref 0 in let d = ref (dist !u) in while !i < size !u do invariant { 0 <= !i <= size(!u) and forall j:int. 0 <= j < size(!u) -> invariant { 0 <= !i <= size !u and forall j:int. 0 <= j < size !u -> !d#j = dist(!u)#j + if repr(!u, j) = r and j < !i then 1 else 0 } variant { size(!u) - !i } if repr !u j = r and j < !i then 1 else 0 } variant { size !u - !i } if ghost_find u !i = r then d := A.store !d !i (A.select !d !i + 1) done; !d { forall i:int. 0 <= i < size(!u) -> result#i = dist(!u)#i + if repr(!u, i) = r then 1 else 0 } { forall i:int. 0 <= i < size !u -> result#i = (dist !u)#i + if repr !u i = r then 1 else 0 } let union (u:uf ref) (a:int) (b:int) = { inv(!u) and 0 <= a < size(!u) and 0 <= b < size(!u) and not same(!u, a, b) } { inv !u and 0 <= a < size !u and 0 <= b < size !u and not same !u a b } let ra = find u a in let rb = find u b in let l = link !u in let d = increment u ra in u := (A.store l ra rb, d, size !u, num !u - 1) { inv(!u) 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) <-> 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) } { inv !u 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 <-> 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 }