Algorithms#
Sections#
An algorithm is a formal procedure for doing some task. An algorithm is a well-defined computational procedure that takes some value or set of values as input and produces some value or set of values as output. An algorithm is a sequence of computational steps that transforms the input into the output. Fast algorithms require that data be stored in a suitable way: this is where data structures come in to play.
Algorithms solve computational problems: computational problems are problems which have well-specified input and output.
2 requirements
Given an input an algorithm should produce the correct output. (CORRECTNESS)
An algorithm should use resources efficiently. (EFFICIENCY)
A data structure is a way of organizing data with associated algorithms for certain tasks. A data structure is a way to store and organize data to facilitate access and modifications.
An abstract data type describes functionality (i.e., which operations are supported).
An implementation is a way to realize the desired functionality. (How is the data stored? array, linked list, etc. Which algorithms implement this operation?)
Describing an algorithm
A complete description of an algorithm consists of three parts.
1. The algorithm itself, in prose, pseudocode, mathematical notation, and perhaps specific implementations
2. A proof of the algorithm’s correctness
3. A derivation of the algorithm’s running time (and auxiliary space requirements)
Proof of Correctness via Loop Invariant
A loop invariant is a condition that is true at the beginning and end of every iteration of a loop.
The precondition describes the possible states of the program just as the loop begins executing.
The postcondition describes the desired states when the loop stops.
To prove correctness with a loop invariant the following things need to be shown.
Initialization
Initialization must show that the invariant is true just after loop initialization but prior to the first iteration of the loop.
In other words, the invariant must be implied by the precondition: If the precondition is true then the invariant is true.
For while loops of the form
while (condition/guard) { body }
the invariant must be true before beginning the loop.
For for loops
for (init; condition/guard; incr) { body }
the invariant must be true just after executing the code init which is not properly part of the loop because it is executed only once.
(i.e., after the initial assignment to the loop-counter variable but before the first test in the loop header)
Maintenance
It must be shown that whenever both the loop invariant and the loop condition are true just before executing the loop body then the loop invariant is true just after executing the loop body. Note that the loop invariant may fail to be true at intermediate steps during the execution of the loop body, as long as it is reestablished by the end. (For for loops, the loop body also includes the increment incr.)
If both the loop condition and the loop invariant are true before iteration then the loop invariant is true after iteration (before the next iteration).
Postcondition
It must be shown that if both the loop condition is false (so that the loop exits) and the loop invariant is true then the loop postcondition is true.
Termination
Termination must show that the loop condition will eventually be false, which means that the loop will eventually exit.
Assuming that the loop invariant is true at the start of each iteration it must be shown that some quantity called the loop variant (or decrementing function) strictly decreases and that it cannot decrease indefinitely.
Let \(\text{DF}\) represent the value of the loop variant. It must be shown that if the loop condition is true then the value of the loop variant after the execution of the loop body \(\text{DF'}\) is strictly less than it was at the beginning:
\(\text{DF'} \lt \text{DF}\)
There must be some minimal value \(\text{DF}_0\) such that if \(\text{DF} \lt \text{DF}_0\) then either the loop condition or loop invariant is false. Since \(\text{DF}\) decreases on every iteration it will eventually be less than \(\text{DF}_0\) at which point the loop must exit.
The field of program verification is concerned with formally proving that programs perform correctly. A program’s correct behavior is defined by stating that if a precondition is true before the program starts then the program will end after a finite number of steps and a postcondition is true after the program ends. A program analyst can show that a large program performs correctly by breaking the program into smaller segments where each segment has a precondition and a postcondition. The postcondition for one segment is the precondition for the next segment. Then for each segment the analyst must prove that if the precondition for that segment is true before the segment executes then the postcondition for the segment is true after the segment executes.
A program segment consisting of a while loop
A while loop has the following form. \(C\) is a loop condition that evaluates to true or false. If the loop condition for a while loop is true then the instructions inside the loop are executed. Otherwise the loop terminates and the next statement after the while loop is executed.
while (C):
list_of_instructions
A loop invariant is an assertion that is true before each iteration of a loop. There are four steps in using a loop invariant to show that a while loop performs correctly. Given a while loop with condition \(C\) and a loop invariant \(I\), the four steps below are sufficient to establish that if the pre-condition is true before the loop then the post-condition is true after the loop.
Show that if the pre-condition is true before the loop begins then \(I\) is also true.
Show that if \(C\) and \(I\) are both true before an iteration of the loop then \(I\) is true after the iteration.
Show that the condition \(C\) will eventually be false.
Show that if \(\lnot C\) and \(I\) are both true then the post-condition is true.
When the first two steps hold, the loop invariant is true prior to every iteration of the loop. Showing that the loop invariant holds before the first iteration of the loop corresponds to the base case and showing that the invariant holds from iteration to iteration corresponds to the inductive step. Mathematical induction typically applies the inductive step infinitely but in a loop invariant the induction stops when the loop terminates.
The first three steps show that the loop satisfies partial correctness: if the loop terminates then it succeeds.
The fourth step shows that the loop satisfies total correctness: the loop eventually terminates.
Constructing a loop invariant#
A loop invariant often makes a statement which depends on \(i\), and about the data seen so far.
What do you want to know at the end of the loop?
Think about a specific iteration: What do you know? What information has been gained by the previous iterations?
Which algorithmic technique are you using? Are you incrementally computing the solution? “At the start of iteration i, answer contains the answer for A[0:i - 1]”