Skip to content

Commit

Permalink
collection/union_find: Add contracts usage
Browse files Browse the repository at this point in the history
Signed-off-by: Florian Deljarry <[email protected]>
  • Loading branch information
Delja committed Oct 1, 2019
1 parent 21de975 commit a117432
Showing 1 changed file with 13 additions and 3 deletions.
16 changes: 13 additions & 3 deletions lib/core/collection/union_find.nit
Original file line number Diff line number Diff line change
Expand Up @@ -88,8 +88,9 @@ class DisjointSet[E]
# Get the root node of an element
# require: `has(e)`
private fun find(e:E): DisjointSetNode
is
expects(nodes.has_key(e))
do
assert nodes.has_key(e)
var ne = nodes[e]
if ne.parent == ne then return ne
var res = nfind(ne)
Expand All @@ -101,6 +102,8 @@ class DisjointSet[E]
# Use *path compression* to flatten the structure
# ENSURE: `result.parent == result`
private fun nfind(ne: DisjointSetNode): DisjointSetNode
is
ensures(result.parent == result)
do
var nf = ne.parent
if nf == ne then return ne
Expand All @@ -126,7 +129,10 @@ class DisjointSet[E]
# Initially it is in its own disjoint subset
#
# ENSURE: `has(e)`
redef fun add(e) do
redef fun add(e)
is
ensures(self.has(e))
do
if nodes.has_key(e) then return
var ne = new DisjointSetNode
nodes[e] = ne
Expand Down Expand Up @@ -199,6 +205,8 @@ class DisjointSet[E]
# Combine the subsets of `e` and `f`
# ENSURE: `in_same_subset(e,f)`
fun union(e,f:E)
is
ensures(in_same_subset(e,f))
do
var ne = find(e)
var nf = find(f)
Expand All @@ -223,8 +231,10 @@ class DisjointSet[E]
end

# Combine the subsets of all elements of `es`
# ENSURE: `all_in_same_subset(cs)`
# ENSURE: `all_in_same_subset(es)`
fun union_all(es:Collection[E])
is
ensures(all_in_same_subset(es))
do
if es.is_empty then return
var f = es.first
Expand Down

0 comments on commit a117432

Please sign in to comment.