26 lines
No EOL
689 B
Text
26 lines
No EOL
689 B
Text
---- MODULE scratch ----
|
|
EXTENDS Naturals, Sequences, FiniteSets
|
|
|
|
IsSorted(seq) ==
|
|
\A i, j \in 1..Len(seq):
|
|
i < j => seq[i] <= seq[j]
|
|
|
|
Range(f) == {f[x] : x \in DOMAIN f}
|
|
|
|
\* Returns the number of values of f(x) matching val
|
|
CountMatching(f, val) ==
|
|
Cardinality({key \in DOMAIN f: f[key] = val})
|
|
|
|
\* That passes the check for IsSorted(Sort(seq)), but is useless:
|
|
\* Sort(seq) == <<>>
|
|
|
|
\* This works
|
|
Sort(seq) ==
|
|
CHOOSE sorted \in [DOMAIN seq -> Range(seq)]:
|
|
\* sorted has the same number of each element as seq
|
|
/\ \A i \in DOMAIN seq:
|
|
CountMatching(seq, seq[i]) = CountMatching(sorted, seq[i])
|
|
/\ IsSorted(sorted)
|
|
|
|
Eval == Sort(<<1, 4, 2, 3>>)
|
|
==== |