I. Predicate functions A. definition ------------------------------------------ PREDICATES def: a *predicate* is a function that ------------------------------------------ B. examples ------------------------------------------ EXAMPLE PREDICATES def odd(n): """Return True just when n is an odd number.""" ------------------------------------------ How would you define the predicate "even"? ------------------------------------------ FOR YOU TO DO Write a predicate, positive(n), that returns True just when n is a positive number. ------------------------------------------ ------------------------------------------ FOR YOU TO DO Write a predicate, strictly_ascending(n1, n2, n3) that returns True just when n1 < n2 and n2 < n3. ------------------------------------------ II. Hoare-style specifications of programs and statements ------------------------------------------ WHY SPECIFY PROGRAMS USING MATH? Usually programs have So ------------------------------------------ What's wrong with asking implementers to generalize from a pattern? A. assertions ------------------------------------------ ASSERTIONS An assertion, such as assert n > 2 is equivalent to if not (n > 2): raise AssertionError() ------------------------------------------ What happens if the expression is true (e.g., if n > 2)? 1. assertions and program states ------------------------------------------ STATES OF A PROGRAM def: a *state* of a program consists of an environment (context) and a heap Notation: a state sigma can be written as a pair of functions (env, heap) env: Variable -> Value heap: Location -> Value Value = Number + Boolean + Location + ... Location = {(o,f) | o is an object, f is a field name} ------------------------------------------ ------------------------------------------ ASSERTIONS CHARACTERIZE SETS OF STATES Boolean assertions (expressions) describe states in which they are True assert n > 2 Which states are passed by this assertion? In general assertions can be used to describe sets of states assert isinstance(n, int) and n > 2 assert op == "and" or op == "or" assert p != None ------------------------------------------ B. pre- and postcondition specifications ------------------------------------------ PRECONDITIONS AND POSTCONDITIONS def: a *precondition* is an assertion that is supposed to be true def: a *postcondition* is an assertion that should be true Partial correctness: postcondition need only be true if the action finishes normally Total correctness: postcondition must be true whenever the action is started in a state satisfying the precondition Example: assert n > 1 # precondition n = n+1 assert n > 2 # postcondition assert isinstance(num, int) s = square(num) assert s == num**2 assert isinstance(gallons, int) ti = teaspoonsIn(gallons) assert math.isclose(ti, 128 * 6 * gallons) ------------------------------------------ ------------------------------------------ PRE- AND POSTCONDITION SPECIFICATIONS ARE MORE EXACTING THAN TESTS compare assert isinstance(gallons, int) ti = teaspoonsIn(gallons) assert math.isclose(ti, 128 * 6 * gallons) to the tests: from math import isclose def test_teaspoonsIn(): assert isclose(teaspoonsIn(1/128), 6.0) assert isclose(teaspoonsIn(1.0), 768.0) assert isclose(teaspoonsIn(0.25), 192.0) assert isclose(teaspoonsIn(0.5), 384.0) assert isclose(teaspoonsIn(10.0), 7680.0) ------------------------------------------ What are the differences between the tests and a pre- and postcondition specification? 1. Design by Contract ------------------------------------------ CONTRACTS Imagine buying a car: dealer: benefit: $5000 (sale price) obligation: provide the car buyer: obligation: provide the $5000 benefit: the car Each side has some benefits and obligations ------------------------------------------ ------------------------------------------ FUNCTION/PROCEDURE CONTRACTS IN SOFTWARE implementation: benefit: assume the precondition obligation: guarantee the postcondition caller: obligation: guarantee the precondition benefit: assume the postcondition Example: square root function: benefit: assume argument is >= 0 obligation: guarantee result >= 0 and result**2 is close to argument def sqrt(arg): assert arg >= 0 # assume precondition # compute res # establish postcondition assert res >= 0 and isclose(result**2, arg) return res caller: obligation: guarantee argument is >= 0 benefit: assume result >= 0 and result**2 is close to argument assert arg >= 0 # establish precondition res = sqrt(arg) # assume postcondition assert res >= 0 and isclose(result**2, arg) ------------------------------------------ ------------------------------------------ CONVENTIONS FOR PRE- AND POSTCONDITIONS IN DOCUMENTATION STRINGS Preconditions: use "Requires P" to say that P is a precondition Postconditions: in functions: use "ensures Q(...result...)" to say that Q is a postcondition in procedures: use "effect Q(...old(arg)...)" to say that Q is a postcondition that describes changes, where old(arg) describes Adapting the syntax of Eiffel to Python: def sqrt(arg): """Requires arg >= 0 and ensures result >= 0 and isclose(result**2, arg)""" # result = ...some computation... return result ------------------------------------------ 2. examples of design by contract ------------------------------------------ ABSTRACTING FROM TEST CASES def test_aroundsun(): assert isclose(aroundsun(1), 2 * pi * AU) assert isclose(aroundsun(18), 36 * pi * AU) assert isclose(aroundsun(19), 38 * pi * AU) assert isclose(aroundsun(20), 40 * pi * AU) assert isclose(aroundsun(30), 60 * pi * AU) assert isclose(aroundsun(40), 80 * pi * AU) assert isclose(aroundsun(50), 100 * pi * AU) # oldest human lived 122 years and 164 days assert isclose(aroundsun(122.449315), 244.89863 * pi * AU) # some turtles and a clam have lived 500 years assert isclose(aroundsun(500), 1000 * pi * AU) # a bristlecone pine is thought to be about 5000 years old assert isclose(aroundsun(5000), 10000 * pi * AU) What would be an appropriate specification for aroundsun(earthyears)? Requires Ensures ------------------------------------------ ------------------------------------------ ANOTHER EXAMPLE def test_average3(): assert isclose(average3(2, 4, 6), 4) assert isclose(average3(50.1, 50.3, 50.2), 50.2) assert isclose(average3(27.0, 2.0, 1.0), 10.0) assert isclose(average3(50.342, 0.0, -50.342), 0.0) # some numbers from the Dow Jones Industrials follow assert isclose(average3(19897.67, 19950.78, 19888.61), 19912.353333333333) assert isclose(average3(15998.08, 17949.37, 19945.04), 17964.163333333333) What's a good specification for average3(n1, n2, n3)? Requires Ensures ------------------------------------------ ------------------------------------------ ANOTHER EXAMPLE def test_teaspoonsIn(): assert isclose(teaspoonsIn(1/128), 6.0) assert isclose(teaspoonsIn(1.0), 768.0) assert isclose(teaspoonsIn(0.25), 192.0) assert isclose(teaspoonsIn(0.5), 384.0) assert isclose(teaspoonsIn(10.0), 7680.0) What would be a good specification for teaspoonsIn(gallons)? Requires Ensures ------------------------------------------ ------------------------------------------ ANOTHER EXAMPLE Sample interaction: 1st price? 99.99 2nd price? 100.00 3rd price? 300.00 Sales tax: $30.00 Total cost: $529.99 What would be a good specification for sales_total()? Requires Effect ------------------------------------------ ------------------------------------------ ANOTHER EXAMPLE Example: number? 5 number? 13 number? 27 number? 42 Yes, these are in strictly ascending order Example: number? 5 number? 13 number? 13 number? 42 No, these are not in strictly ascending order What would be a good specification for the procedure isascending()? Requires Effect ------------------------------------------ C. Axioms for statements ------------------------------------------ DEFINEDNESS OF EXPRESSIONS For an expression E defined(E) means that the evaluation of E will not result in an error/exception or non-termination E.g., defined(n/d) == (d != 0) ------------------------------------------ 1. primitive statements ------------------------------------------ AXIOM SCHEMAS FOR STATEMENTS IN PYTHON A way to describe the semantics of statements, (total correctness interpretation) Pass: assert P pass assert P Assignment: assert ------------------------------------------ ------------------------------------------ FUNCTION AND PROCEDURE CALLS Function call: Suppose f(arg1,...,argn) has specification requires P(arg1,...,argn) ensures Q(result,arg1,...,argn) assert Procedure call: Suppose p(arg1,...,argn has specifications requires P(arg1,...,argn) ensures Q(arg1,...,argn,old(arg1),...,old(argn)) assert ------------------------------------------ ------------------------------------------ ASSERT STATEMENTS An assert statement is similar to pass when the condition is true: assert E assert E assert E ------------------------------------------ Is assert E1 and E2 the same as executing assert E1 followed by assert E2? 2. compound statements ------------------------------------------ SUITES (COMPOUND STATEMENTS) Suppose assert P1 S1 assert Q and assert Q S2 assert Q2 then: ------------------------------------------ What role does Q play in the sequence? ------------------------------------------ CONDITIONAL STATEMENTS Suppose assert defined(E) and E S1 assert Q and assert defined(E) and not E S2 assert Q then: ------------------------------------------ Why does this work? What S1 and S2 don't produce the same postcondition? 3. rule of consequence ------------------------------------------ RULE OF CONSEQUENCE Suppose assert P S assert Q then: assert P' S assert Q' holds, provided Why? ------------------------------------------ D. Examples ------------------------------------------ THE MAXIMUM FUNCTION Write a function maximum(n1, n2) that satisifes the specification: Requires isinstance(n1, numbers.Number) and isinstance(n2, numbers.Number) Ensures (result == n1 or result == n2) and result >= n1 and result >= n2 def maximum(n1, n2) assert isinstance(n1, numbers.Number) assert isinstance(n2, numbers.Number) ------------------------------------------ What kind of statement do we need to write to make the postcondition true? Why? III. Friday Problems with Boolean Expressions and Predicates A. implication function ------------------------------------------ FOR YOU TO DO 1. Write a function, implies(b1, b2), that takes two bool arguments, b1 and b2, and returns True just when b1 implies b2. That is, it returns true just when either not b1 or b2 is True. ------------------------------------------ B. printing truth tables for arbitrary functions ------------------------------------------ FOR YOU TO DO 2. Write a procedure, print_truth_table(p), that takes a 2-argument Boolean predicate, p, as an argument, and prints a truth table for p that displays the value of p(b1, b2) for all pairs of Booleans b1 and b2. For example, print_truth_table(implies) would print on stdout: arg1\arg2 | True | False True | True | False False | True | True For another example, suppose we have: def notOrDM(b1, b2): return not (b1 or b2) == not b1 and not b2 Then print_truth_table(notOrDM) would print on stdout: arg1\arg2 | True | False True | True | True False | True | True ------------------------------------------ C. tautologies ------------------------------------------ FOR YOU TO DO 3. Write a function, is_tautology(p), that takes a 2-argument Boolean predicate, p, as an argument and returns True just when p is a tautology. That is is_tautology(p) returns True just when p(True,True), p(True, False), p(False, True), and p(False, False) are all True. ------------------------------------------