=> F T Q -- P=>Q F T T T F T P
-- PRE: N >= 1 first := 1; last := 1; startRun := 1; for i from 2 to N do -- INV: a[first..last] the longest nondec' run in a[1..i-1] -- and a[startRun..i-1] is non decreasing if a[i] < a[i-1] then -- end of last run startRun := i; else -- a[i] >= a[i-1] if i-startRun > last-start then -- breaks record first := startRun; last := i end_if; end_if; end_for -- assert: a[first..last] is the longest non-decreasing -- run in a[1..i-1] and i=N+1, hence desired outcome.
© L . A l l i s o n 2 0 0 0 |
C o m p S c i M o n a s h |
A u s t r a l i a |
if x < y then if x < z then -- x < y and x < z small := x else -- z <= x < y small := z end_if else -- y <= x if z < y then -- z < y <= x small := z else -- y <= z and y <= x small := y end_if end_ifThis particular code always carries out two comparisons.
min := a[1]; for i from 2 to N do -- INV: 1<=j<i => min<=a[j] if a[i] < min then min := a[i] end_if end_for -- assert: (1<=j<i => min<=a[j]) and i=N+1 -- so: 1<=j<=N => min<=a[j]Note, we leave out, as "obvious", that min is in a[1..i-1], but if we were being "picky" we would include this too.
0 0 0 0 1 1 1 ? ? ? ? ? ? 2 2 4 4 4 4 4 4 ^ ^ ^ ^ | | | | p q r sa) Invent a suitable invariant describing the 5 sections of the array, possibly empty, 4 coloured, and one unknown but shrinking.
find(x, T, current) if T is empty then return current elsif element(T) < x then return find(x, right(T), current) elsif element(T) > x then return find(x, left(T), min(element(T), current)) else -- equal return element(T) end_if initial call: find(k, T, infinity) -- e.g. can use maxint for infinity over ints
© 2000, L. Allison, Comp. Sci. & SWE, Monash University, Australia