A. Programming Concepts and Skills · Algorithm Design and AnalysisSpecifying Algorithms: Preconditions, Postconditions and Loop Invariants
C2.1 A4.2About 70 minutes
Learning goals- I can state the precondition (starting state) and postcondition (ending state) of an algorithm.
- I can write a precondition and postcondition in a docstring and check a precondition with assert or an exception.
- I can find a loop invariant and use it to explain why an algorithm reaches its postcondition.
- I can predict what goes wrong when a precondition is not met.
Words to know
precondition
What must be true before an algorithm runs (its starting state) for it to work correctly.
postcondition
What the algorithm guarantees is true when it finishes (its ending state), as long as the precondition held.
contract
The agreement between a caller and a function: the caller makes the precondition true, and the function then makes the postcondition true.
loop invariant
A statement that is true before the loop starts and stays true after every pass of the loop.
assertion
A statement in code (assert) that checks a condition and stops the program with an AssertionError if it is false.
side effect
A change a function makes outside its return value, such as changing a list it was given or printing.
A promise with fine print
A snow-clearing company promises: "Your driveway will be clear by 7 a.m." Read the fine print: if the snowfall is under 30 cm and your car is not parked in the driveway. The fine print is the precondition. The promise is the postcondition.
Algorithms work the same way. Before you can measure how fast an algorithm is (the next lessons), you need to be able to say exactly what it does and when it works. That is the job of preconditions and postconditions. This lesson is the base for the whole unit: every search, sort and recursive algorithm you write here will start with a clear statement of its starting and ending states.
Remember from Grade 11
In Algorithms to Specification: Inserting and Deleting in a Sorted Array (ICS3U) you read a specification whose precondition was "the list is sorted in ascending order" and whose postcondition was "the list contains the new value and is still sorted". Now you will analyse these conditions for any algorithm, and use them to argue that the algorithm is correct.
Starting state and ending state
The precondition describes the starting state: what must be true about the inputs (and anything else the algorithm reads) before it begins. The postcondition describes the ending state: what is true about the return value and the data when it finishes.
Together they form a contract:
- The caller is responsible for making the precondition true.
- The function is responsible for making the postcondition true, provided the precondition was true.
- If the caller breaks the precondition, the function promises nothing. It might crash, loop forever, or (worst of all) return a wrong answer quietly.
A good postcondition also says what the function does not change. "The list a is unchanged" is part of the contract, because a caller may rely on it.
index_of_max. The precondition (left) is the caller's job; the postcondition (right) is the function's promise. If the left box is false, the right box is not guaranteed.Writing the contract down
Professional programmers put the contract in the function's docstring, the documentation string right under the def line. Here is a function that finds the position of the largest element, written with its contract.
def index_of_max(a):
"""Return the index of the largest element of a.
Precondition: a is a list of numbers and len(a) >= 1.
Postcondition: returns the smallest index i such that
a[i] >= a[k] for every index k; a is unchanged.
"""
best = 0
for i in range(1, len(a)):
if a[i] > a[best]:
best = i
return best
print(index_of_max([4, 9, 2, 9, 1]))
Output: 1. There are two 9s. The postcondition says smallest index, and > (not >=) keeps the first 9, so the answer is 1.
Why "smallest index"?
A precise postcondition settles every question in advance. With two equal largest values, should the function return 1 or 3? The contract says 1. A tester can now write a test for that case, and anyone who changes > to >= (which would return 3) breaks the contract. Vague postconditions such as "returns the biggest" lead to arguments and bugs.
What if the precondition is broken?
Call index_of_max([]). The loop runs zero times and the function returns 0, but there is no element 0. The caller then does a[0] and gets an IndexError far away from the real cause. A function can check its precondition so the failure happens at the right place:
assert len(a) >= 1, "a must not be empty" checks a condition that should never be false if the program is correct. It is a tool for catching programmer mistakes while developing and testing.raise ValueError("...") is for bad data that can really happen when the program runs, for example a user typing nothing. The caller can catch it with try/except (you met exceptions in ICS3U).
def average(values):
"""Return the arithmetic mean of values.
Precondition: values is a non-empty list of numbers.
Postcondition: returns sum(values) / len(values); values is unchanged.
"""
assert len(values) > 0, "average() needs at least one value"
return sum(values) / len(values)
print(average([12, 15, 21]))
print(average([]))
The first call meets the precondition and prints 16.0. The second call breaks it, so the program stops with AssertionError: average() needs at least one value instead of a confusing ZeroDivisionError.
assert is not input validation
Python skips every assert when it is run with the -O (optimize) option, so never use assert to check user input or file data. Use if and raise ValueError(...), or ask again. Use assert for conditions that are true in a correct program: preconditions between your own functions, loop invariants and test checks.
Loop invariants: the idea that proves a loop works
How do you know index_of_max is right for every list, not only the ones you tested? Find a loop invariant: a statement that is
- true before the loop starts (initialization),
- still true after each pass if it was true before that pass (maintenance), and
- useful when the loop ends: together with the reason the loop stopped, it gives the postcondition (termination).
For index_of_max the invariant is: at the start of each pass with index i, a[best] is the largest of a[0] to a[i − 1], and best is the first place it occurs.
- Before the loop: i = 1 and best = 0. The only element checked is a[0], so it is the largest. True.
- Each pass: if a[i] is bigger, best moves to i; otherwise best stays. Either way a[best] is the largest of a[0] to a[i]. True for the next i.
- At the end: i has gone past the last index, so the "checked part" is the whole list. That is exactly the postcondition.
index_of_max([4, 9, 2, 9, 1]). At every row the invariant holds: the yellow cell is the largest of the shaded cells. On the last row the whole list is shaded, so the invariant becomes the postcondition.Worked exampleAnalysing a contract
Here is a function that is supposed to count how many times a value appears in a sorted list by stopping early:
def count_sorted(a, x):
count = 0
for v in a:
if v == x:
count += 1
elif v > x:
break
return count
State its precondition and postcondition, and show what happens if the precondition is broken with a = [5, 1, 5] and x = 5.
- Inputs it reads: a list
a and a value x. The loop stops as soon as it sees a value bigger than x. That shortcut is only safe if every later value is also bigger, which is true when a is sorted in ascending order. - Precondition:
a is a list sorted in ascending order, and x can be compared with its elements. - Postcondition: returns the number of indexes k with
a[k] == x; a is unchanged (the function only reads it). - Broken precondition: with
[5, 1, 5], v = 5 matches (count = 1); v = 1 is not equal and not bigger, so the loop continues; v = 5 matches (count = 2). The answer 2 happens to be right! - Try
a = [5, 9, 5]: v = 5 (count = 1), then v = 9 > 5, so the loop breaks. It returns 1, but there are two 5s. The function returns a wrong answer without any error, the most dangerous kind of failure.
Precondition: a is sorted ascending. Postcondition: returns how many elements equal x, and a is unchanged. Unsorted input can give a silently wrong count (1 instead of 2 for [5, 9, 5]), which is why the precondition must be stated and, while testing, checked.
Analysing any algorithm: a checklist
When you are asked to analyse the precondition and postcondition of an algorithm:
- List every input it reads (parameters, global values, files).
- For each line, ask: what must be true for this line to work? (An index must be in range; a divisor must not be 0; a shortcut needs sorted data.) These become the precondition.
- Describe the return value exactly, including ties, empty cases and "not found".
- Say what the function changes (side effects) and what it leaves unchanged.
- Test the edges: the smallest legal input, and one input that breaks each part of the precondition.
Just for funPrecondition for enjoying this joke: you have read the previous section.
Postcondition: you groan. (If you did not groan, the precondition was not met. Please re-read the section, then the joke.)
Hands-on activityContract cards for three functions
You need: a computer with Python, 3 index cards (or a sheet of paper folded into three), and a pen.
- Pick three functions you can write in a few lines:
index_of_min(a), is_sorted(a) (returns True if every element is ≤ the next one), and remove_all(a, x) (removes every copy of x from the list a, changing a). - On each card, write the precondition on the front and the postcondition on the back before you write any code. Be exact: ties? empty list? what changes?
- Code each function with its contract in the docstring, and an
assert that checks the precondition where it makes sense. - Swap cards with a family member. Ask them to suggest an input that might break the function ("What about an empty list?"). Run it. Did the contract cover it?
- For
index_of_min, write the loop invariant as a comment above the loop, and add assert lines that check it on each pass, for example assert a[best] == min(a[:i]) at the top of the loop body. Run it on 5 different lists. Then delete the invariant checks (they make the loop slow).
What to look for: is_sorted([]) and is_sorted([7]) should both return True (there is no pair out of order), and remove_all should say in its postcondition that the order of the remaining elements is unchanged.
Your turn
1What is the difference between a precondition and a postcondition?
A precondition is what must be true before the algorithm runs (starting state). A postcondition is what the algorithm guarantees after it finishes (ending state), if the precondition was true.
2Write a precondition for def divide_evenly(total, people): return total // people.
total and people are integers and people > 0 (so there is no ZeroDivisionError, and negative people make no sense).
3Write a postcondition for a function is_sorted(a) that returns True or False.
Returns True if and only if a[k] <= a[k + 1] for every index k from 0 to len(a) − 2; otherwise returns False. a is unchanged.
4Who is responsible for making the precondition true: the function or the caller?
The caller. The function only promises its postcondition when the precondition holds.
5A function sorts the list it is given in place and returns None. Write its postcondition.
The list a contains the same elements as before (same values, same counts), now in ascending order, and the function returns None.
6Why is assert a bad way to check that a user typed a positive number?
Asserts can be switched off (python -O), and an AssertionError is a crash, not a friendly message. User input should be checked with if and handled (ask again, or raise ValueError and catch it).
7Give the three properties a loop invariant must have to prove a loop correct.
It is true before the loop starts; each pass keeps it true; and when the loop ends, the invariant plus the stopping condition gives the postcondition.
More practice: warm-up
1True or false: if the precondition is broken, the function must raise an error.
False. The function promises nothing; it may crash, loop forever, or return a wrong answer.
2Name the starting state and the ending state using the course vocabulary.
Starting state: precondition. Ending state: postcondition.
3What is a side effect? Give one example.
A change outside the return value, for example changing a list passed in, printing, or writing to a file.
4Write an assert that checks that a list scores is not empty, with a message.
assert len(scores) > 0, "scores must not be empty" (or assert scores, ...).
5What does index_of_max([3, 3, 3]) return, using the code in the lesson?
0. No later element is strictly bigger, so best never moves.
More practice: on your own
1State a precondition and postcondition for def last_char(s): return s[-1].
Precondition: s is a string with len(s) ≥ 1 (an empty string gives IndexError). Postcondition: returns the last character of s; s is unchanged (strings are immutable anyway).
2This function is meant to return the index of x in a, or −1:
def find(a, x):
for i in range(len(a)):
if a[i] == x:
return i
Which part of a sensible postcondition does it fail, and how do you fix it?
When x is not in a, the loop ends and the function falls off the end, returning None instead of −1. Add return -1 after the loop (not inside it).
3Give a loop invariant for this loop, which adds up a list:
total = 0
for i in range(len(a)):
total += a[i]
At the start of each pass with index i, total equals a[0] + a[1] + … + a[i − 1] (the sum of the elements already visited). Before the loop, i = 0 and total = 0 (the empty sum). At the end, total is the sum of the whole list.
4def middle(a): return a[len(a) // 2]. What is the precondition? Which element does it return for a list of length 4?
Precondition: len(a) ≥ 1. For length 4, 4 // 2 = 2, so it returns a[2], the later of the two middle elements; the postcondition should say so.
5A function remove_first(a, x) removes the first copy of x from a. Write a complete postcondition, including the case where x is missing.
If x was in a, the first occurrence is removed, the length drops by 1, and the order of the other elements is unchanged. If x was not in a, a is unchanged. (Alternatively, make "x is in a" a precondition; either is fine as long as it is stated.)
Challenge
1Selection sort's outer loop (from ICS3U) has index p. State a loop invariant that, at the end, gives "the list is sorted".
At the start of pass p: a[0..p − 1] holds the p smallest elements of the list, in ascending order, and the rest of the list holds the remaining elements. Initially p = 0 (empty part, true). Each pass moves the smallest remaining element to index p, keeping it true. When p reaches n − 1, the first n − 1 smallest are in place, so the last is the largest and the whole list is sorted.
2A program calls count_sorted(scores, 70) from the worked example right after scores.append(new_score). Explain the bug and two ways to fix it.
append adds to the end, so if new_score is smaller than the last element the list is no longer sorted, breaking the precondition; the count can be wrong without any error. Fix 1: insert new_score in its sorted position instead of appending (or sort after appending). Fix 2: use a counting function with no precondition on order, such as scores.count(70).
3Prove with a loop invariant that this function returns True exactly when a contains no negative number:
def all_non_negative(a):
i = 0
while i < len(a) and a[i] >= 0:
i += 1
return i == len(a)
Invariant: a[0] … a[i − 1] are all ≥ 0. Before the loop i = 0 (nothing checked: true). The loop only increases i after checking a[i] ≥ 0, so it stays true. The loop stops when i == len(a) (then the whole list is non-negative, return True) or when a[i] < 0 with i < len(a) (a negative exists, return False). The loop always ends because i increases each pass and cannot pass len(a).
Quiz
1. Which statement describes a postcondition?
2. def ratio(a, b): return a / b. Which is the best precondition?
3. If a caller breaks a function's precondition, what does the contract guarantee?
4. When should a program use raise ValueError rather than assert?
5. For the summing loop total += a[i] over i = 0 to n − 1, which is a correct loop invariant at the start of each pass?
6. count_sorted([5, 9, 5], 5) from the lesson returns 1. Why?
Big idea: This lesson covers C2.1 (analysing the precondition, or starting state, and postcondition, or ending state, of an algorithm). It also starts A4.2, because a precise contract tells you exactly which test cases to write.
How to help: Ask your teen to explain one of their functions to you as a "deal": "If you give me ___, I promise to give you ___." Then ask, "What if I give you an empty list? Two equal values? Nothing at all?" Each question they cannot answer is a gap in the contract.
Common difficulties:
- Writing postconditions that describe how the code works ("loops through the list") instead of what is true at the end.
- Forgetting ties, empty inputs and the "not found" case.
- Using
assert to validate user input. - Choosing an invariant that is true only at the end (such as "total is the sum of the whole list"), instead of one that is true on every pass.