[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
enrich
Bubblesort-col,
Bubblesort-row,
Bubblesort-row-rev
,
nat-pot,
nat-even
with
functions
#clean0rows : matrix(tord) × tord → nat;
comment: #clean0rows counts the number of initial rows where all elements are < i;
#clean1rows : matrix(tord) × tord → nat;
comment: #clean0rows counts the number of final rows where all elements are ≥ i;
#dirtyrows : matrix(tord) × tord → nat;
comment: clean0rows counts the the rows between clean1 and clean0 rows;
log2↑ : nat → nat;
comment: ⌈log_2(n)⌉, the smallest natural number greater or equal to real-valued log_2(n), 1 for 0;
countevn : array(tord) × (tord → bool) → nat;
comment: count all elements that satisfy p with even index ;
countodd : array(tord) × (tord → bool) → nat;
comment: count all elements that satisfy p with odd index ;
predicates
srowsorted : matrix(tord) × nat × matrix(tord);
comment: second matrix(tord) is a version of the first one one with first n rows sorted;
colsorted : matrix(tord) × nat × matrix(tord);
comment: second matrix(tord) is a version of the first one with first n colums sorted;
rowsincreasing : matrix(tord) × nat;
comment: the elements in row n are bigger than all elements in smaller rows;
. .dirtyrows≤ ( . ) : matrix(tord) × nat;
comment: the number of dirty rows = all rows - all< - all≥ ;
procedures psortrows# : matrix(tord) nonfunctional nondeterministic;
psortrowssnake# : matrix(tord) nonfunctional nondeterministic;
psortrowsnake# nat × bool : matrix(tord) nonfunctional nondeterministic;
psortcols# : matrix(tord) nonfunctional nondeterministic;
pshearsort# : matrix(tord) nonfunctional nondeterministic;
variables
mx : matrix(tord);
a : array(tord);
i : tord;
j : tord;
m : nat;
n : nat;
r : nat;
c : nat;
bound : nat;
asc : bool;
p : tord → bool;
MX : matrix(tord) flexible;
M : nat flexible;
N : nat flexible;
R : nat flexible;
C : nat flexible;
ASC : bool flexible;
ORD : tord × tord → bool flexible;
partial functions
. /↑ . : nat × nat → nat prio 11 right with λ m, n. n ≠ 0;
comment: whole number division, but rounding up, not down;
countevn : array(tord) × nat × nat × (tord → bool) → nat with λ a, m, n, p. m ≤ n ∧ n ≤ # a;
comment: count all elements that satisfy p with even index between lower and upper bound;
countodd : array(tord) × nat × nat × (tord → bool) → nat with λ a, m, n, p. m ≤ n ∧ n ≤ # a;
comment: count all elements that satisfy p with odd index between lower and upper bound;
axioms
countevn-base: m ≤ # a ⊦ countevn(a, m, m, p) = 0;
used for: s, ls;
countevn-rec: m ≤ n, n ≤ # a ⊦ countevn(a, m, n + 1, p) = countevn(a, m, n, p) + (even(n) ∧ p(a[n]) ⊃ 1;0);
used for: s, ls;
countevn-def: countevn(a, p) = countevn(a, 0, # a, p);
countodd-base: m ≤ # a ⊦ countodd(a, m, m, p) = 0;
used for: s, ls;
countodd-rec: m ≤ n, n ≤ # a ⊦ countodd(a, m, n + 1, p) = countodd(a, m, n, p) + (odd(n) ∧ p(a[n]) ⊃ 1;0);
used for: s, ls;
countodd-def: countodd(a, p) = countodd(a, 0, # a, p);
divup-def: m /↑ n = (∃ n0. m = n0 * n ⊃ m / n;m / n + 1);
log2up-def: log2↑(n) = (∃ m. n = 2^ m ⊃ log2 n;log2(2 * n + 1));
dirtyrows-def: #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx;
clean0rows-bounded: ¬ #r mx < #clean0rows(mx, i);
used for: las;
clean0rows-notallls: #clean0rows(mx, i) < #r mx → count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0;
clean0rows-allls: r < #clean0rows(mx, i) → count(mx[r]r, λ j. ¬ j < i) = 0;
clean1rows-bounded: ¬ #r mx < #clean1rows(mx, i);
used for: las;
clean1rows-notallge: #clean1rows(mx, i) + r + 1 = #r mx → count(mx[r]r, λ j. j < i) ≠ 0;
clean1rows-allge: #r mx ≤ #clean1rows(mx, i) + r ∧ r < #r mx → count(mx[r]r, λ j. j < i) = 0;
dirtyrowsbound-def: mx.dirtyrows≤(bound) ↔ (∀ i. #dirtyrows(mx, i) ≤ bound);
rowno-updrow: #c mx = # a, r < #r mx ⊦ #r mx[r, a]r = #r mx;
used for: ls;
rowno-updcol: #r mx = # a, c < #c mx ⊦ #r mx[c, a]c = #r mx;
used for: ls;
colno-updrow: #c mx = # a, r < #r mx ⊦ #c mx[r, a]r = #c mx;
used for: ls;
colno-updcol: #r mx = # a, c < #c mx ⊦ #c mx[c, a]c = #c mx;
used for: ls;
colsorted-def:
m ≤ #c mx
→ ( colsorted(mx0, m, mx)
↔ #r mx = #r mx0 ∧ #c mx = #c mx0
∧ (∀ c. c < #c mx → (c < m ⊃ perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c);mx0[c]c = mx[c]c)));
srowsorted-def:
m ≤ #r mx
→ ( srowsorted(mx0, m, mx)
↔ #r mx = #r mx0 ∧ #c mx = #c mx0
∧ (∀ r. r < #r mx → (r < m ⊃ perm(mx0[r]r, mx[r]r) ∧ ordered≤((even(r) ⊃ mx[r]r;rev(mx[r]r)));mx0[r]r = mx[r]r)));
rowsincreasing-def:
rowsincreasing(mx, r) ↔ (∀ r1, r2, c1, c2. r1 < r2 ∧ r2 < r ∧ c1 < #c mx ∧ c2 < #c mx → ¬ mx[r2, c2] < mx[r1, c1]);
comment: all elements in row r1 are less or equal to all elements in row r2 when r1 < r2 < r;
declarations
psortrows:
psortrows#(; MX){forall∥nf R with R < #r MX do psortrow#(R; MX)};
psortcols:
psortcols#(; MX){forall∥nf C with C < #c MX do psortcol#(C; MX)};
psortrowssnake:
psortrowssnake#(; MX){forall∥nf M with M < #r MX do psortrowsnake#(M, even(M); MX)};
psortrowsnake:
psortrowsnake#(M, ASC; MX){if ASC then psortrow#(M; MX) else psortrowrev#(M; MX)};
pshearsort:
pshearsort#(; MX)
{let N = log2↑(#r MX)
in {/* invariant perm(MX`.toArr, MX.toArr) ∧ #c MX = #c MX` ∧ #r MX = #r MX` ∧ #c MX ≠ 0
∧ MX.dirtyrows≤(#r MX /↑ 2^(N` - N)) ∧ N ≤ N` ∧ (N = 0 → colsorted(MX, #c MX, MX))
wfbound N */;
while N > 0
do {/* use contract psortrowssnake-correct and skip call */; psortrowssnake#(; MX); /* use contract psortcols-correct and skip call */;
psortcols#(; MX); N := N - 1}};
/* use contract psortrows-correct and skip call */; psortrows#(; MX)
};
end enrich