COMP 250 Lecture Notes - Lecture 9: Loop Invariant, Postcondition, Precondition

• School: McGill University
• Department: Computer Science (Sci)
• Course: COMP 250
• Professor: Mathieu Blanchette

Document Summary

An algorithm is described by: input data, output data, preconditions: specifies restrictions on input data. Data must have for algorithm to produce right answer: postconditions: specifies what is the result. State in which we want to leave the algorithm. An algorithm is correct if: for any correct input data it stops and it produces correct output, if correct input satisfies precondition, if correct output data satisfies postcondition. *can be complicated to prove correctness when there are loops or repetition. A loop property that holds before and after each iteration of a loop. M a[0] while(i m), then m remains unchanged and is the min of {a[0] a[i]} After increasing i by 1, m is the min {a[0] a[i-1]}: termination, algorithm will stop. Counter variable i is constantly being increased by 1.