stdlib: set library revamped

parent 9f605136
:x: marks a potential source of incompatibility
Standard library
* set library revamped
- set.Fset
type `set` -> type `fset` and `choose` -> `pick`
- `appset.Appset` -> `set.SetApp` and `impset.Impset` -> `set.SetImp`
type `t` -> `set` and `.contents` -> `.to_fset`
`empty` -> `empty ()`
Tools
* why3prove counterexamples output is not JSON by default. To restore previous
behavior, pass the argument --json
......
......@@ -278,21 +278,6 @@ module mach.int.State63
syntax val random_int63 "REMOVE"
end
module set.Fset
syntax val mem "REMOVE"
syntax val (==) "REMOVE"
syntax val subset "REMOVE"
syntax val is_empty "REMOVE"
syntax val empty "REMOVE"
syntax val add "REMOVE"
syntax val remove "REMOVE"
syntax val union "REMOVE"
syntax val inter "REMOVE"
syntax val diff "REMOVE"
syntax val choose "REMOVE"
syntax val cardinal "REMOVE"
end
module mach.peano.Peano
syntax type t "int"
syntax val to_int "Z.of_int %1"
......
......@@ -298,21 +298,16 @@ theory set.Set
remove prop mem_empty
syntax function add "add(%1, %2)"
remove prop add_spec
syntax function singleton "singleton(%1)"
syntax function remove "remove(%1, %2)"
remove prop remove_spec
remove prop subset_remove
syntax function union "union(%1, %2)"
remove prop union_spec
syntax function inter "intersection(%1, %2)"
remove prop inter_spec
syntax function diff "difference(%1, %2)"
remove prop diff_spec
remove prop subset_diff
(* TODO: choose *)
......@@ -321,7 +316,7 @@ theory set.Set
end
theory set.Fset
syntax type set "finite_set[%1]"
syntax type fset "finite_set[%1]"
syntax predicate mem "member(%1, %2)"
remove prop extensionality
......@@ -331,24 +326,25 @@ theory set.Fset
syntax function empty "(emptyset :: %t0)"
syntax predicate is_empty "empty?(%1)"
remove prop empty_def
remove prop is_empty_empty
remove prop empty_is_empty
syntax function add "add(%1, %2)"
remove prop add_spec
remove prop add_def
syntax function singleton "singleton(%1)"
syntax function remove "remove(%1, %2)"
remove prop remove_spec
remove prop remove_def
remove prop subset_remove
syntax function union "union(%1, %2)"
remove prop union_spec
remove prop union_def
syntax function inter "intersection(%1, %2)"
remove prop inter_spec
remove prop inter_def
syntax function diff "difference(%1, %2)"
remove prop diff_spec
remove prop diff_def
remove prop subset_diff
(* TODO: choose *)
......
......@@ -363,29 +363,30 @@ module WP
use Imp
use set.Fset as Set
clone set.SetApp as S with type elt = ident, val eq = Int.(=)
predicate assigns (sigma:env) (a:Set.set ident) (sigma':env) =
predicate assigns (sigma:env) (a:Set.fset ident) (sigma':env) =
forall i:ident. not (Set.mem i a) ->
IdMap.get sigma i = IdMap.get sigma' i
lemma assigns_refl:
forall sigma:env, a:Set.set ident. assigns sigma a sigma
forall sigma:env, a:Set.fset ident. assigns sigma a sigma
lemma assigns_trans:
forall sigma1 sigma2 sigma3:env, a:Set.set ident.
forall sigma1 sigma2 sigma3:env, a:Set.fset ident.
assigns sigma1 a sigma2 /\ assigns sigma2 a sigma3 ->
assigns sigma1 a sigma3
lemma assigns_union_left:
forall sigma sigma':env, s1 s2:Set.set ident.
forall sigma sigma':env, s1 s2:Set.fset ident.
assigns sigma s1 sigma' -> assigns sigma (Set.union s1 s2) sigma'
lemma assigns_union_right:
forall sigma sigma':env, s1 s2:Set.set ident.
forall sigma sigma':env, s1 s2:Set.fset ident.
assigns sigma s2 sigma' -> assigns sigma (Set.union s1 s2) sigma'
predicate stmt_writes (i:stmt) (w:Set.set ident) =
predicate stmt_writes (i:stmt) (w:Set.fset ident) =
match i with
| Sskip | Sassert _ -> true
| Sassign id _ -> Set.mem id w
......@@ -394,19 +395,19 @@ predicate stmt_writes (i:stmt) (w:Set.set ident) =
end
let rec compute_writes (s:stmt) : Set.set ident
let rec compute_writes (s:stmt) : S.set
ensures {
forall sigma pi sigma' pi':env, n:int.
many_steps sigma pi s sigma' pi' Sskip n ->
assigns sigma result sigma' }
variant { s }
= match s with
| Sskip -> Set.empty
| Sassign i _ -> Set.singleton i
| Sseq s1 s2 -> Set.union (compute_writes s1) (compute_writes s2)
| Sif _ s1 s2 -> Set.union (compute_writes s1) (compute_writes s2)
| Sskip -> S.empty ()
| Sassign i _ -> S.singleton i
| Sseq s1 s2 -> S.union (compute_writes s1) (compute_writes s2)
| Sif _ s1 s2 -> S.union (compute_writes s1) (compute_writes s2)
| Swhile _ _ s -> compute_writes s
| Sassert _ -> Set.empty
| Sassert _ -> S.empty ()
end
val fresh_from_fmla (q:fmla) : ident
......
......@@ -14,8 +14,8 @@ theory Graph
(* the graph is defined by a set of vertices and a set of edges *)
type vertex
constant vertices: set vertex
constant edges: set (vertex, vertex)
constant vertices: fset vertex
constant edges: fset (vertex, vertex)
predicate edge (x y: vertex) = mem (x,y) edges
......@@ -144,7 +144,7 @@ module BellmanFord
use Graph
use int.IntInf as D
use ref.Ref
clone impset.Impset as S with type elt = (vertex, vertex)
clone set.SetImp as S with type elt = (vertex, vertex)
clone impmap.ImpmapNoDom with type key = vertex
type distmap = ImpmapNoDom.t D.t
......@@ -159,7 +159,7 @@ module BellmanFord
(* [inv1 m pass via] means that we already performed [pass-1] steps
of the main loop, and, in step [pass], we already processed edges
in [via] *)
predicate inv1 (m: distmap) (pass: int) (via: set (vertex, vertex)) =
predicate inv1 (m: distmap) (pass: int) (via: fset (vertex, vertex)) =
forall v: vertex. mem v vertices ->
match m[v] with
| D.Finite n ->
......@@ -180,7 +180,7 @@ module BellmanFord
forall lu: list vertex. path s lu u -> length lu >= pass)
end
predicate inv2 (m: distmap) (via: set (vertex, vertex)) =
predicate inv2 (m: distmap) (via: fset (vertex, vertex)) =
forall u v: vertex. mem (u, v) via ->
D.le m[v] (D.add m[u] (D.Finite (weight u v)))
......@@ -222,7 +222,7 @@ module BellmanFord
)
let relax (m: distmap) (u v: vertex) (pass: int)
(ghost via: set (vertex, vertex))
(ghost via: fset (vertex, vertex))
requires { 1 <= pass /\ mem (u, v) edges /\ not (mem (u, v) via) }
requires { inv1 m pass via }
ensures { inv1 m pass (add (u, v) via) }
......@@ -265,8 +265,8 @@ module BellmanFord
}
end
val get_edges (): S.t
ensures { result.S.contents = edges }
val get_edges (): S.set
ensures { result = edges }
exception NegativeCycle
......@@ -286,9 +286,9 @@ module BellmanFord
invariant { inv1 m i empty }
let es = get_edges () in
while not (S.is_empty es) do
invariant { subset es.S.contents edges /\ inv1 m i (diff edges es.S.contents) }
invariant { subset es.S.to_fset edges /\ inv1 m i (diff edges es.S.to_fset) }
variant { S.cardinal es }
let ghost via = diff edges es.S.contents in
let ghost via = diff edges es.S.to_fset in
let (u, v) = S.choose_and_remove es in
relax m u v i via
done;
......@@ -297,7 +297,7 @@ module BellmanFord
assert { inv1 m (cardinal vertices) empty };
let es = get_edges () in
while not (S.is_empty es) do
invariant { subset es.S.contents edges /\ inv2 m (diff edges es.S.contents) }
invariant { subset es.S.to_fset edges /\ inv2 m (diff edges es.S.to_fset) }
variant { S.cardinal es }
let (u, v) = S.choose_and_remove es in
if D.lt (D.add m[u] (D.Finite (weight u v))) m[v] then begin
......
This diff is collapsed.
theory Th1
use set.Fsetint
use set.FsetInt
(* proved with vampire 0.6 and eprover 1.4 *)
lemma l_false : false
end
theory Th2
use set.Fsetint
use set.FsetInt
function integer : set int
function integer : fset int
lemma mem_integer: forall x:int. mem x integer
goal foo : false
......
......@@ -14,15 +14,15 @@
module CoincidenceCount
use int.Int
use array.Array
use ref.Refint
use set.Fsetint
use set.FsetComprehension
use set.FsetInt
function setof (a: array 'a) : set 'a =
function setof (a: array 'a) : fset 'a =
map (fun x -> a[x]) (interval 0 (length a))
function drop (a: array 'a) (n: int) : set 'a =
function drop (a: array 'a) (n: int) : fset 'a =
map (fun x -> a[x]) (interval n (length a))
lemma drop_left:
......@@ -36,11 +36,11 @@ module CoincidenceCount
cardinal (inter (setof a) (setof b))
lemma not_mem_inter_r:
forall a: array int, i: int, s: set int. 0 <= i < length a ->
forall a: array int, i: int, s: fset int. 0 <= i < length a ->
not (mem a[i] s) -> inter (drop a i) s == inter (drop a (i+1)) s
lemma not_mem_inter_l:
forall a: array int, i: int, s: set int. 0 <= i < length a ->
forall a: array int, i: int, s: fset int. 0 <= i < length a ->
not (mem a[i] s) -> inter s (drop a i) == inter s (drop a (i+1))
let coincidence_count (a b: array int) : int
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<why3session shape_version="6">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file proved="true">
<path name=".."/>
<path name="coincidence_count.mlw"/>
<theory name="CoincidenceCount" proved="true">
<goal name="drop_left" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.15" steps="288"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="0.15" steps="207"/></proof>
</goal>
<goal name="not_mem_inter_r" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="162"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="688"/></proof>
</goal>
<goal name="not_mem_inter_l" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="162"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="678"/></proof>
</goal>
<goal name="VC coincidence_count" expl="VC for coincidence_count" proved="true">
<proof prover="0"><result status="valid" time="0.62" steps="2222"/></proof>
<proof prover="0"><result status="valid" time="6.22" steps="11544"/></proof>
</goal>
</theory>
</file>
......
......@@ -16,7 +16,7 @@
module CoincidenceCount
use list.List
use set.Fset
use set.SetAppInt
use list.Elements
use list.Mem as L
use int.Int
......@@ -24,7 +24,7 @@ module CoincidenceCount
clone export list.Sorted
with type t = int, predicate le = (<), goal Transitive.Trans
let rec coincidence_count (a b: list int) : set int
let rec coincidence_count (a b: list int) : set
requires { sorted a }
requires { sorted b }
ensures { result == inter (elements a) (elements b) }
......@@ -39,7 +39,7 @@ module CoincidenceCount
else
coincidence_count a tb
| _ ->
empty
empty ()
end
end
......@@ -49,7 +49,6 @@ end
module CoincidenceCountAnyType
use list.List
use set.Fset
use list.Elements
use list.Mem as L
use int.Int
......@@ -58,6 +57,9 @@ module CoincidenceCountAnyType
val predicate eq (x y : t)
ensures { result <-> x = y }
clone set.SetApp with type elt = t, val eq = eq
val predicate rel (x y : t)
clone relations.TotalStrictOrder with type t, predicate rel, axiom .
......@@ -65,7 +67,7 @@ module CoincidenceCountAnyType
clone export list.Sorted
with type t = t, predicate le = rel, goal Transitive.Trans
let rec coincidence_count (a b: list t) : set t
let rec coincidence_count (a b: list t) : set
requires { sorted a }
requires { sorted b }
ensures { result == inter (elements a) (elements b) }
......@@ -80,7 +82,7 @@ module CoincidenceCountAnyType
else
coincidence_count a tb
| _ ->
empty
empty ()
end
end
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<why3session shape_version="6">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../coincidence_count_list.mlw" proved="true">
<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="10" steplimit="0" memlimit="4000"/>
<prover id="2" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<file proved="true">
<path name=".."/>
<path name="coincidence_count_list.mlw"/>
<theory name="CoincidenceCount" proved="true">
<goal name="Transitive.Trans" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="VC coincidence_count" expl="VC for coincidence_count" proved="true">
<proof prover="0"><result status="valid" time="2.20" steps="9025"/></proof>
<transf name="split_vc" proved="true" >
<goal name="VC coincidence_count.0" expl="variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC coincidence_count.1" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC coincidence_count.2" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC coincidence_count.3" expl="variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC coincidence_count.4" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC coincidence_count.5" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC coincidence_count.6" expl="variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC coincidence_count.7" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC coincidence_count.8" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC coincidence_count.9" expl="postcondition" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC coincidence_count.9.0" expl="postcondition" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC coincidence_count.9.0.0" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="1.97" steps="19829"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</theory>
<theory name="CoincidenceCountAnyType" proved="true">
<goal name="SetApp.VC eq" expl="VC for eq" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Transitive.Trans" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="VC coincidence_count" expl="VC for coincidence_count" proved="true">
<proof prover="0"><result status="valid" time="0.65" steps="4363"/></proof>
<proof prover="0"><result status="valid" time="2.49" steps="10258"/></proof>
</goal>
</theory>
<theory name="CoincidenceCountList" proved="true">
......
......@@ -9,7 +9,6 @@ module DijkstraShortestPath
use int.Int
use ref.Ref
use set.Fset
(** The graph is introduced as a set v of vertices and a function g_succ
returning the successors of a given vertex.
......@@ -18,16 +17,16 @@ module DijkstraShortestPath
type vertex
clone impset.Impset as S with type elt = vertex
clone set.SetImp with type elt = vertex
clone impmap.ImpmapNoDom with type key = vertex
constant v: Fset.set vertex
constant v: fset vertex
val ghost function g_succ (x: vertex) : Fset.set vertex
ensures { Fset.subset result v }
val ghost function g_succ (x: vertex) : fset vertex
ensures { subset result v }
val get_succs (x: vertex): S.t
ensures { result.S.contents = g_succ x }
val get_succs (x: vertex): set
ensures { result = g_succ x }
val function weight vertex vertex : int (* edge weight, if there is an edge *)
ensures { result >= 0 }
......@@ -36,7 +35,7 @@ module DijkstraShortestPath
(* The set of already visited vertices. *)
val visited: S.t
val visited: set
(* Map d holds the current distances from the source.
There is no need to introduce infinite distances. *)
......@@ -45,44 +44,44 @@ module DijkstraShortestPath
(* The priority queue. *)
val q: S.t
val q: set
predicate min (m: vertex) (q: S.t) (d: t int) =
S.mem m q /\
forall x: vertex. S.mem x q -> d[m] <= d[x]
predicate min (m: vertex) (q: set) (d: t int) =
mem m q /\
forall x: vertex. mem x q -> d[m] <= d[x]
val q_extract_min () : vertex writes {q}
requires { not S.is_empty q }
requires { not is_empty q }
ensures { min result (old q) d }
ensures { q.S.contents = Fset.remove result (old q.S.contents) }
ensures { q = remove result (old q) }
(* Initialisation of visited, q, and d. *)
val init (src: vertex) : unit writes { visited, q, d }
ensures { S.is_empty visited }
ensures { q.S.contents = Fset.singleton src }
ensures { is_empty visited }
ensures { q = singleton src }
ensures { d = (old d)[src <- 0] }
(* Relaxation of edge u->v. *)
let relax u v
ensures {
(S.mem v visited /\ q = old q /\ d = old d)
(mem v visited /\ q = old q /\ d = old d)
\/
(S.mem v q /\ d[u] + weight u v >= d[v] /\ q = old q /\ d = old d)
(mem v q /\ d[u] + weight u v >= d[v] /\ q = old q /\ d = old d)
\/
(S.mem v q /\ (old d)[u] + weight u v < (old d)[v] /\
(mem v q /\ (old d)[u] + weight u v < (old d)[v] /\
q = old q /\ d = (old d)[v <- (old d)[u] + weight u v])
\/
(not S.mem v visited /\ not S.mem v (old q) /\
q.S.contents = Fset.add v (old q.S.contents) /\
(not mem v visited /\ not mem v (old q) /\
q = add v (old q) /\
d = (old d)[v <- (old d)[u] + weight u v]) }
= if not S.mem v visited then
= if not mem v visited then
let x = d[u] + weight u v in
if S.mem v q then begin
if mem v q then begin
if x < d[v] then d[v] <- x
end else begin
S.add v q;
add v q;
d[v] <- x
end
......@@ -99,7 +98,7 @@ module DijkstraShortestPath
forall x: vertex. path x x 0
| Path_cons:
forall x y z: vertex. forall d: int.
path x y d -> Fset.mem z (g_succ y) -> path x z (d + weight y z)
path x y d -> 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
......@@ -109,7 +108,7 @@ module DijkstraShortestPath
lemma Path_inversion:
forall src v:vertex. forall d:int. path src v d ->
(v = src /\ d = 0) \/
(exists v':vertex. path src v' (d - weight v' v) /\ Fset.mem v (g_succ v'))
(exists v':vertex. path src v' (d - weight v' v) /\ mem v (g_succ v'))
lemma Path_shortest_path:
forall src v: vertex. forall d: int. path src v d ->
......@@ -123,84 +122,84 @@ module DijkstraShortestPath
v = src /\ d > 0
\/
exists v': vertex. exists d': int.
shortest_path src v' d' /\ Fset.mem v (g_succ v') /\ d' + weight v' v < d
shortest_path src v' d' /\ mem v (g_succ v') /\ d' + weight v' v < d
lemma Completeness_lemma:
forall s: S.t.
forall s: set.
(* if s is closed under g_succ *)
(forall v: vertex.
S.mem v s -> forall w: vertex. Fset.mem w (g_succ v) -> S.mem w s) ->
mem v s -> forall w: vertex. mem w (g_succ v) -> mem w s) ->
(* and if s contains src *)
forall src: vertex. S.mem src s ->
forall src: vertex. mem src s ->
(* then any vertex reachable from s is also in s *)
forall dst: vertex. forall d: int.
path src dst d -> S.mem dst s
path src dst d -> mem dst s
(* Definitions used in loop invariants. *)
predicate inv_src (src: vertex) (s q: S.t) =
S.mem src s \/ S.mem src q
predicate inv_src (src: vertex) (s q: set) =
mem src s \/ mem src q
predicate inv (src: vertex) (s q: S.t) (d: t int) =
predicate inv (src: vertex) (s q: set) (d: t int) =
inv_src src s q /\ d[src] = 0 /\
(* S and Q are contained in V *)
Fset.subset s.S.contents v /\ Fset.subset q.S.contents v /\
subset s v /\ subset q v /\
(* S and Q are disjoint *)
(forall v: vertex. S.mem v q -> S.mem v s -> false) /\
(forall v: vertex. mem v q -> mem v s -> false) /\
(* we already found the shortest paths for vertices in S *)
(forall v: vertex. S.mem v s -> shortest_path src v d[v]) /\
(forall v: vertex. mem v s -> shortest_path src v d[v]) /\
(* there are paths for vertices in Q *)
(forall v: vertex. S.mem v q -> path src v d[v])
(forall v: vertex. mem v q -> path src v d[v])
predicate inv_succ (src: vertex) (s q: S.t) (d: t int) =
predicate inv_succ (src: vertex) (s q: set) (d: t int) =
(* successors of vertices in S are either in S or in Q *)
forall x: vertex. S.mem x s ->
forall y: vertex. Fset.mem y (g_succ x) ->
(S.mem y s \/ S.mem y q) /\ d[y] <= d[x] + weight x y
forall x: vertex. mem x s ->
forall y: vertex. mem y (g_succ x) ->
(mem y s \/ mem y q) /\ d[y] <= d[x] + weight x y
predicate inv_succ2 (src: vertex) (s q: S.t) (d: t int) (u: vertex) (su: S.t) =
predicate inv_succ2 (src: vertex) (s q: set) (d: t int) (u: vertex) (su: set) =
(* 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. Fset.mem y (g_succ x) ->
(x<>u \/ (x=u /\ not (S.mem y su))) ->
(S.mem y s \/ S.mem y q) /\ d[y] <= d[x] + weight x y
forall x: vertex. mem x s ->
forall y: vertex. mem y (g_succ x) ->
(x<>u \/ (x=u /\ not (mem y su))) ->
(mem y s \/ mem y q) /\ d[y] <= d[x] + weight x y
lemma inside_or_exit:
forall s, src, v, d. S.mem src s -> path src v d ->
S.mem v s
forall s, src, v, d. mem src s -> path src v d ->
mem v s
\/
exists y. exists z. exists dy.
S.mem y s /\ not (S.mem z s) /\ Fset.mem z (g_succ y) /\
mem y s /\ not (mem z s) /\ mem z (g_succ y) /\
path src y dy /\ (dy + weight y z <= d)
(* Algorithm's code. *)
let shortest_path_code (src dst: vertex)
requires { Fset.mem src v /\ Fset.mem dst v }
ensures { forall v: vertex. S.mem v visited ->
requires { mem src v /\ mem dst v }
ensures { forall v: vertex. mem v visited ->
shortest_path src v d[v] }
ensures { forall v: vertex. not S.mem v visited ->
ensures { forall v: vertex. not mem v visited ->
forall dv: int. not path src v dv }
= init src;
while not S.is_empty q do
while not is_empty q do
invariant { inv src visited q d }
invariant { inv_succ src visited q d }
invariant { (* vertices at distance < min(Q) are already in S *)
forall m: vertex. min m q d ->
forall x: vertex. forall dx: int. path src x dx ->
dx < d[m] -> S.mem x visited }
variant { Fset.cardinal v - S.cardinal visited }
dx < d[m] -> mem x visited }
variant { cardinal v - cardinal visited }
let u = q_extract_min () in
assert { shortest_path src u d[u] };
S.add u visited;
add u visited;
let su = get_succs u in
while not S.is_empty su do
invariant { Fset.subset su.S.contents (g_succ u) }
while not is_empty su do
invariant { subset su (g_succ u) }
invariant { inv src visited q d }
invariant { inv_succ2 src visited q d u su }
variant { S.cardinal su }
let v = S.choose_and_remove su in
variant { cardinal su }
let v = choose_and_remove su in
relax u v;
assert { d[v] <= d[u] + weight u v }
done
......
This diff is collapsed.
......@@ -25,12 +25,12 @@ module Esterel
use int.Int
use int.MinMax
use set.Fsetint
use set.FsetInt
use bv.BV64
type s = {
bv : BV64.t; (* a 64-bit bitvector *)
ghost mdl: set int; (* its interpretation as a set *)
ghost mdl: fset int; (* its interpretation as a set *)
}
invariant {
forall i: int. (0 <= i < size /\ nth bv i) <-> mem i mdl
......
......@@ -14,32 +14,28 @@
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC union" expl="VC for union" proved="true">
<proof prover="6"><result status="valid" time="0.16" steps="221"/></proof>
<proof prover="6"><result status="valid" time="0.16" steps="439"/></proof>
</goal>
<goal name="VC intersection" expl="VC for intersection" proved="true">
<proof prover="6"><result status="valid" time="0.06" steps="189"/></proof>
<proof prover="6"><result status="valid" time="0.06" steps="311"/></proof>
</goal>
<goal name="VC aboveMin" expl="VC for aboveMin" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC aboveMin.0" expl="precondition" proved="true">
<proof prover="4" timelimit="1" memlimit="1000"><result status="valid" time="0.01"/></proof>
<goal name="VC aboveMin.0" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.15" steps="399"/></proof>
</goal>
<goal name="VC aboveMin.1" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.15" steps="307"/></proof>
<proof prover="7"><result status=