Porovnanie dvoch neklesajúcich postupností
dané 2 postupnosti f, g
f: ? ? i: 0 ? i ? N :: f[i] ? f[i + 1] ?
g: ? ? i: 0 ? i ? N :: g[i] ? g[i + 1] ?
Úloha: zistit, ci { f[i] | 0 ? i ? N } = { g[i] | 0 ? i ? N }
predpokladáme, ze f[0] = g[0], f[N] = g[N] a tiez ze f[N] resp. g[N] sú väcšie ako ostatné cleny (dá sa to zarucit tak, ze polozíme f[0] = g[0] = ?? a f[N] = g[N] = ?)
invariant I
0 ? u ? N ? 0 ? v ? N ?
? { f[i] | 0 ? i ? u } = { g[i] | 0 ? i ? v }
Program Compare
declare u, v: int
initially u, v = 0, 0
assign
u := u + 1 if u < N ? f[u] = f[u + 1]
v := v + 1 if v < N ? g[v] = g[v + 1]
u, v := u + 1, v + 1
if u < N ? v < N ? f[u + 1] = g[v + 1]
FP ? (u ? N ? f[u] ? f[u + 1]) ?
(v ? N ? g[v] ? g[v + 1]) ?
(u ? N ? v ? N ? f[u + 1] ? g[v + 1])