algorithm = takes one-or-more values, produces an outputs Ex: contains Given a list of L and value v, return v \in L. Input: L is an array, v is a value Output: true if v \in L, false otherwise i, r := 0, false while i neq |L| do if L[i] = v then r := true i := i + 1 else i := i + 1 return r invariants Induction hypothesis that holds at beginning of iteration.
Hypothesis: holds after j-th, j<m repetition of loop
Step: assume inv holds when start m-th loop, proves it holds again at the end of m-th loop
Are we done?
Assuming invariant → does it reach conclusion
Does it end?
Formal argument: prove a bound function
bound function f on the state of the algorithm such that the output of f
natural number (0, 1, 2, …)
strictly decreases after each iteration
f=∣L∣−i starts at ∣L∣,∣L∣≥0
correctness.
pre-condition: restriction require on input
post-condition: should the output be
prove the running the program turns pre-condition and post-condition
complexity.
assume V is not in the listContains(N) = 5 + 7N
given V is in the list
contains is correct, runtime complexity is ContainsRuntime(|L|)=∣L∣ and memory complexity is ContainsMemory(|L|)=1
runtime.
figure1: graph comparison
models are simplification.
shows different growth rates.
Interested in scalability of algorithm
For large enough inputs, contains will always be faster than altc because order of growth of CRuntime<AltCRuntimefigure2: Growth
