Below are two approaches to your problem.
detailed semi-formal proof
Since you've provided a minimal context, I will state my assumptions then provide a solution.
Moreover, I will use very basic loops rather than the fancy for-each loop since they are easier
to prove correctness with ─more accurately, easier for me with my current knowledge.
- We are assuming simple undirected graphs: ie., pairs
(V, E) of a set V of vertices
and a symmetric relation E ⊆ V × V.
- Two vertices are “connected” precisely when there is a path along
E between the two:
x ~ y ∶≡ (∃ n : ℕ • x Eⁿ y) ─where the bullet serves to separate the bound variable
of the quantifier and the body of the quantifier, and exponentiation is iterated relational
product.
A “connected component” is a subgraph in which any two vertices are connected, and which
is connected to no additional vertices in the supergraph. For our needs, we only
consider connected components arising from subsets of vertices.
𝒞 connected-component
⇔ (∀ x,y : 𝒞 • x ~ y) ∧ (∀ 𝒟 : ℙ V • 𝒞 ⊆ 𝒟 ∧ (∀ x,y : 𝒟 • x ~ y) ⇒ 𝒞 = 𝒟)
⇔ (∀ 𝒟 : ℙ V • (∀ x,y : 𝒟 • x ~ y) ∧ 𝒞 ⊆ 𝒟 ⇔ 𝒟 ⊆ 𝒞)
⇔ 𝒞 is an ~-equivalence class
Note that ∧ means “and”.
Make-set assigns the emptyset ∅ to each vertex, in some look-up table.
We assume this to be the case at the very beginning and so need not worry about it.
Find-set looks up the set that is associated to a vertex, in the aforementioned look-up table.
Union(x,y) alters the set associated to x by unioning it what the set associated to y,
and does so as well for y. In particular, after this command we have
Find-set x = old-Find-set x ∪ old-Find-set y.
The post-condition of the program is
∀ x : V •
Find-set x = {y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ E xᵢ₊₁))}
i.e.,
∀ x : V • connected-component (Find-set x)
That is, the algorithm assigns the connected components to the associated sets of the vertices.
Alternatively, it is: Find-set x = the ~-equivalence class of x.
From the post-condition,
∀ x : V •
Find-set x = {y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ E xᵢ₊₁))}
The simplest thing to do is to replace a constant, say E, with a new variable, and relate it
to the constant to obtain an invariant.
P ∷ 𝓔 ⊆ E ∧
(∀ x : V •
Find-set x
= {y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ 𝓔 xᵢ₊₁))})
So it is obvious that the post-condition is obtained once we've arrived at the conclusion
E ⊆ 𝓔. So a good idea is to increase 𝓔 until this condition is true.
Moreover, the invaraint needs to hold before the loop and we can do this by setting
𝓔 ≔ ∅: indeed ∅ ⊆ E and intially every vertex is assigned the emptyset which is what
is needed since,
{y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ 𝓔 xᵢ₊₁)))}
=⟨ initial value of 𝓔 ⟩
{y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ ∅ xᵢ₊₁)))}
=⟨ definition of empty set ⟩
{y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • false))}
=⟨ “for all i, we have false ≡ false” ⟩
{y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ false)}
=⟨ “false ∧ stuff ≡ false” ⟩
{y : V ❙ (∃ x₀,…,xₙ : V • false)}
=⟨ “there is some stuff yielding false ≡ false” ⟩
{y : V ❙ false }
=⟨ there are no y that make false true ⟩
∅
=⟨ initial value of Find-set ⟩
Find-set x
So, to be very explicit, we assume that before the algorithm is run, we have
∀ x : V • find-set x = ∅.
Anyhow, the previous paragraph informs us that the algorithm we are looking for has the shape
{Pre: (∀ x : V • find-set x = ∅) }
𝓔 ≔ ∅
; {Invariant: 𝓔 ⊆ E ∧
(∀ x : V • Find-set x = {y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ 𝓔 xᵢ₊₁))}) }
while ¬ E ⊆ 𝓔 : do-stuff
{Post: (∀ x : V • Find-set x = {y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ E xᵢ₊₁))}
Note that it is common to place “assert” statements within curly braces.
C♯ for example documents them in the form Contract.Assert.IsTrue(...).
It seems the only thing left to do is find an implementation of do-stuff.
Well, the loop terminates if we make the loop guard ¬ E ⊆ 𝓔 false.
By the invariant, we know ♯𝓔 ≤ ♯E and so increasing 𝓔 will do the job.
We can choose an edge of E, it doesn't matter which one as long as it's one we haven't
considered it, and add that to 𝓔. What, are there even such edges!?
Well, by the invariant, we have 𝓔 ⊆ E ∧ E ⊈ 𝓔 within the loop, which implies
E - 𝓔 ≠ ∅, whence there are such edges.
Hence, one possible candidate for do-stuff is
(u,v) ≔ choose an edge from E - 𝓔
; 𝓔 ≔ 𝓔 ∪ {(u,v)}
The candidate is enough and we are done deriving our algorithm, “provided” that this choice
of do-stuff does not ruin the invariant.
It clearly does ruin the invariant since we have not altered the find-set for these two
vertices.
The final result is
{Pre: (∀ x : V • find-set x = ∅) }
𝓔 ≔ ∅
; {Invariant: 𝓔 ⊆ E ∧
(∀ x : V • Find-set x = {y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ 𝓔 xᵢ₊₁))}) }
while ¬ E ⊆ 𝓔 :
(u,v) ≔ choose an edge from E - 𝓔
; if find-set u ≠ find set u then union(u,v)
; 𝓔 ≔ 𝓔 ∪ {(u,v)}
{Post: (∀ x : V • Find-set x = {y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ E xᵢ₊₁))}
To relate this to your initial code, consider the following.
for each i in S : do-stuff
≈
visited ≔ ∅
; while visited ≠ S:
i ≔ pick an element of S - visited
; do-stuff
; visited ≔ visited ∪ {i}
Our loop had ¬ E ⊆ 𝓔 and this is tantamount to E ≠ 𝓔:
E ≠ 𝓔
=⟨ bi-containment ⟩
¬(E ⊆ 𝓔 ∧ 𝓔 ⊆ E)
=⟨ invariant ⟩
¬(E ⊆ 𝓔 ∧ true)
=⟨ “stuff ∧ true ≡ true” ⟩
¬ E ⊆ 𝓔
We use basic while loops since they are easier to work with is all.
I've never really learned to write correctness proofs for for-each loops.
Hope this helps!
Bi-implication informal argument
The algorithm's post-condition is
find-set x = {y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ E xᵢ₊₁))}.
We show the equality using a bi-implication.
(⊆) ∷
By the construction of find-set, i.e., the way we add elements to the set associated to x,
we know that any added element is connected to x and so
find-set x ⊆ {y : V ❙ (∃ x₀,…,xₙ : V • x = x₀ ∧ xₙ = y ∧ (∀ i • xᵢ E xᵢ₊₁))}.
(⊇) ∷
We will show by induction that any vertex y at-least n : ℕ edges away from
x must be within find-set x.
Base case: n = 0. Then x = x₀ = xₙ = y and clearly y ∈ find-set x.
Inductive step: if x E x₁ E x₂ E ⋯ E xₙ E xₙ₊₁ = y then by the inductive hypothesis
xₙ ∈ find-set x; moreover, the algorithm ensures find-set x = find-set xₙ.
Now since (xₙ, xₙ+1) is an edge ─a given─, the algorithm ensures
find-set xₙ₊₁ = find-set xₙ but by the previous equalities we then have
y ∈ find-set y = find-set xₙ₊₁ = find-set xₙ = find-set x.
:-)
