48 lines
1009 B
Plaintext
48 lines
1009 B
Plaintext
predicate sorted(s: seq<int>)
|
|
{
|
|
forall i,j: int :: 0 <= i < j < |s| ==> s[i] <= s[j]
|
|
}
|
|
|
|
predicate sameElements(a: seq<int>, b: seq<int>)
|
|
{
|
|
multiset(a) == multiset(b)
|
|
}
|
|
|
|
method SelectionSort(a: array<int>)
|
|
modifies a
|
|
ensures sorted(a[..])
|
|
ensures sameElements(a[..], old(a[..]))
|
|
{
|
|
if (a.Length == 0) {
|
|
return;
|
|
}
|
|
|
|
var s := 0;
|
|
|
|
while (s < a.Length - 1)
|
|
invariant sameElements(a[..], old(a[..]))
|
|
invariant forall i,j: int :: 0 <= i < s <= j < a.Length ==> a[i] <= a[j]
|
|
invariant s <= a.Length - 1
|
|
invariant s >= 1 ==> sorted(a[0..s])
|
|
decreases a.Length - s
|
|
{
|
|
var min: int := s;
|
|
var i: int := s + 1;
|
|
|
|
while i < a.Length
|
|
invariant sameElements(a[..], old(a[..]))
|
|
invariant s <= min < a.Length
|
|
invariant s + 1 <= i <= a.Length
|
|
invariant forall j: int :: s <= j < i ==> a[min] <= a[j]
|
|
decreases a.Length - i
|
|
{
|
|
if (a[i] < a[min]) {
|
|
min := i;
|
|
}
|
|
i := i + 1;
|
|
}
|
|
|
|
a[s], a[min] := a[min], a[s];
|
|
s := s + 1;
|
|
}
|
|
} |