CSC236H5 Lecture Notes - Lecture 7: University Of Toronto Mississauga, Postcondition, Precondition
8 Nov 2017
School
Department
Course
Professor
Document Summary
For a) this won"t be correct if it doesn"t terminate def f(x): while true: pass. For d) precondition is always false; this means that there is no acceptable way to call this function. For each program path from the first line to a return statement, we show that it terminates and satisfies the postcondition. If there are no recursive calls, analyze the code directly. By the induction hypothesis, you can assume that the recursive call satisfies the post-condition. If there is a loop, use loop variants and invariants def . Post: returns the factorial of n if else : return . Post: returns the factorial of n if n <= 1: return 1 return n * fact_rec(n-1) else: If n= 0, path 1 returns 1. and 0! = 1, so the correct value is returned. If n=1, path 1 returns 1. 1! = 1, so the correct value is returned.
