# Principled Programming / Tim Teitelbaum / Chapter 3. import math import sys # 1. Statement Specifications. # 1.1. Implementations. def e3_1_1() -> None: # Output the square of an integer that is provided as input data. n: int = int(input()); print(n * n) def e3_1_2() -> None: # Output the square of an integer that is provided as input data. # Note. It makes no difference whether the two statements are on the # same line (as above) or on different lines (as below). n: int = int(input()) print(n * n) def e3_1_3() -> None: # Output the square of an integer that is provided as input data. n: int = int(input()) # Let s be the square of n. s: int = n * n print(s) def e3_1_4() -> None: # Output the square of an integer that is provided as input data. n: int = int(input()) # Let s be the square of n. s: int = 0 for k in range(0,n): s = s + n print(s) # 1.2. Specification Style. def e3_2_1() -> None: # Input integer n, and output n squared. # Note. There is no variable n. n is just a pronoun. print(int(input()) ** 2) def e3_2_2() -> None: # Input integer x, and output the number n such that n*n=x. # Note. There are no variables x or n. They are just pronouns. # Note. The output is a float, because Math.sqrt returns a float. print(math.sqrt(int(input()))) # 1.3. Specifications as Higher-Level Code. def e3_3_1() -> None: # x: int = 10 y: int = 20 print(x, y) # Swap x and y. temp: int = x x = y y = temp # print(x, y) # 1.4. What? Not how? def e3_4_1() -> None: # Sample array A[0..4] consisting of 10, 20, 30, 40, and 50. A: list[int] = [10, 20, 30, 40, 50] n: int = 5 # Length of test array A. v: int # Test value input as test data. # while True: # v = int(input()) # Find v in A[0..n-1]. Given array A[0..n-1], n≥0, and value v, let k be # smallest nonnegative integer s.t. A[k]==v, or let k==n if there are no # occurrences of v in A. k: int = 0 # Start k at the left end of array A. while (k < n and # Stop as soon as k runs off the right end of A, or A[k] != v ): # as soon as A[k]==v. k += 1 # Step one place to the right. # print(k) # 1.5. States and Effects. # The text lists situations that you can assume will not occur, and therefore # don't have to remark on in a specification. Nonetheless, they can occur, # as demonstrated below. # Demonstrate the rule: # No declaration conflicts. Fresh variable declarations will not interfere with # already-existing variables with the same name. def e3_5_1() -> None: # Declare n and initialize it to 0. n: int = 0 # Let n be 1. # Note that our specifications are amibiguous on whether a fresh # variable is required. In Python, even if an implementation appears to # declare a fresh variable, it doesn't do so, and the pre-existing instance # of a variable with the same name prevails. n: int = 1 # Print the contents of n. print(n) # prints 1. # Demonstrate the rule: # Memory sufficiency. The computer memory has space for any new variables required. def e3_5_2() -> None: # Print the largest integer that is allowed as in int. print(sys.maxsize) # Declare an array A with that many array elements (too much memory required). A: list[int] = [0] * sys.maxsize # Throws "MemoryError" exception. A[0] = 0 # Demonstrate the rule: # No side effects. Unmentioned preexisting variables must not be changed, and no # input or output operations occur other than what is mentioned. def e3_5_3() -> None: # Let y = 1. y: int = 1 # Let x = 0. x: int = 0 y = 0 # The specification say nothing about y, and therefore this is impopper. # Print x and y. print(x) # Prints 0. print(y) # According to the specifications, this should print 1, # but prints 0 due to spurious assignment to y. # Demonstrate the rule: # Termination. Execution completes unless an unending process is explicitly specified. # This can fail in two ways: # (1) You have specified an unending process, but it actually terminates. # (2) You have specfied a terminating process, but it runs forever. def e3_5_4() -> None: # (1) Specification: Do not under any circumstances print "done". # (under the faulty assumption that the halving loop will run forever) h: float = 10 while h > 0: h = h / 2 # The loop is not infinite. Rather, h reaches 5e-324, and that # divided by 2 is smaller than the smallest positive float, # so the quotient is zero, and the loop terminates.d print(h) # Prints 0.0 # (2) Specification: print "done". # (under the faulty assumption that the doubling loop will not run forever, # because k will eventually hit some maximum, k will equal k_old, and the while will stop.) # The code is commented out because it would run forever. ## k_old: int = 0 ## k: int = 10 ## while k != k_old: ## print(k) ## k_old == k ## k = k * 2 ## print("done") # Demonstrate the rule: # Syntactic adequacy. The implementation must have appropriate syntax for the # context in which it occurs. def e3_5_5() -> None: # Due to the interpretation of indentation in Python, this rule cannot be followed. # Rather, the context must adapt to the specification and the indentation of its # implementation. Arguably, the following and its implementation are correct: # # # print "2.1" and then print "2.2". # print("2.1"); print("2.2") # # but when inserted between the following two lines of code: # # print("1.0") # print("3.0") # # the meaning of the code and its implementation changes to: # "Unexpected indent" pass # Demonstrate the rule: # Numerical magnitudes. Numerical input data fit in whatever type of program # variables the program chooses to use for them. def e3_5_6() -> None: # Given a float input f, echo f to the output. # Enter 1e100, and program output correctly echos the input. # Enter 1e1000, and the program output echos "inf". f: float = float(input()) print(f) # Python stores an int in a manner the places no limit on its magnitude # other than the amount of available memory. Thus, this is not an issue for integers. # enter 123456789012345678901234567890, and the program output echos the input exactly. k: int = int(input()) print(k) # Demonstrate the rule: # Numerical precision. Requirements stated as if values were infinite precision # reals may hold only approximately when implemented as floating-point values. def e3_5_7() -> None: # Output the number n such that n*n=x. # Prints 8.881784197001252E-16, and then fails the assertion. x: float = 7 n: float = math.sqrt(x) print(n * n - x) assert n * n == x, "imprecision due to finite floating-point representation" # 1.6. Conditions and Sets of States. # Confirm that relatively obscure code for swap works # for all pairs of 32-bit int values between -100 and 100. def e3_6_1() -> None: lo: int = -100 hi: int = +100 for j in range(lo, hi): for k in range(lo, hi): # x: int = j; y: int = k # Swap x and y. x = x + y y = x - y x = x - y # if x != k or y != j: print("Failure") print("Success.") # 1.7. Assertions. # Demonstrate a method protected from a bad argument by the system's builtin zero-divide check. # Given n!=0, return x//n. def nth(x: int, n: int) -> int: return x // n def e3_7_1() -> None: # Compute n!=0 such that blah blah. n: int = 0 # A bug. # Given n!=0, let y be the nth part of x. x: int = 10 y: int = nth(x, n) # print(y) print("no exception thrown") # Demonstrate the use of an assert when no builtin check will protect you (as it did in e3_7_1). def e3_7_2() -> None: # Compute n!=0 such that blah blah. n: int = 0 # A bug. # Given n!=0, do Whatever. assert n != 0, "blah blah computed a zero n" print("no assertion failure") # Demonstrate the equivalent of an assert using a conditional and System.exit(). def e3_7_3() -> None: # Compute n!=0 such that blah blah. n: int = 0 # A bug. # Given n!=0, do Whatever. if n == 0: print("blah blah computed a zero n") sys.exit(0) print("no assertion failure") # Demonstrate how floating point uses extended values to defer exceptions. def e3_7_4() -> None: # Compute n!=0 such that blah blah. n: float = 1e-300 # A bug. # Given n!=0, let y be the nth part of x. x: float = 1e300 y: float = x/n # execution time later. print(y) # Prints inf. z: float = y-1 print(z) # Prints inf w: float = 1/y print(w) # Prints 0.0 print("no exception thrown") # Prints "no exception thrown" # 2. Declaration Assertions. # 3. Method Specifications. def max(x: int, y: int) -> int: """Return the larger of the values x and y.""" if x < y: return y else: return x def validate_non_decreasing(A: list[int]) -> bool: """Return True iff A is in non-decrerasing order.""" # n: int = len(A) # Set k to the least index for which A[k] is greater than A[k+1], or n-1 if ordered. k: int = 0 while (k < n - 1) and (A[k] <= A[k + 1]): k += 1 # return k == n - 1 def sort(A: list[int], n: int): """Rearrange array A[0..n-1] to be in non-decreasing order.""" assert A is not None, "Null array A." assert n >= 0, "Negative n." assert n <= len(A), "n bigger than length of A." A.sort() # Library sorting algorithm. assert validate_non_decreasing(A) def e3_8_1() -> None: A: list[int] = [ 0, 2, 4, 1, 3, 5] sort(A,6) # Output array A on a line. for k in range(0, 6): print(str(A[k]) + " ", end='') print() # Output array A using builtin representation of list. print(A) # Each of the following lines would generate an exception if not commented out. # sort(None, 0) # sort(A,-1) # sort(A, 10) # B: list[int] = [0, 2, 4, 1, 3, 5] # print(find(B,6,2)) # Demonstrate correct working of sort and binary search (find). B: list[int] = [ 0, 2, 4, 1, 3, 5] sort(B,6) print(find(B,6,2)) def find(A: list[int], n: int, v: int) -> int: """ Given int array A[0..n-1] sorted in non-decreasing order, and int v, return an index where A[k]==v, or return n if v does not occur in A. Note the incongruety in a log n binary search algorithm of a linear-time validation that argument A is ordered . Clearly, this would only remain in the code during development, as it subverts the performance purpose of binary search. """ # assert A is not None, "Null array A." assert n >=0, "Negative n." assert n <= len(A), "n bigger than length of A." assert validate_non_decreasing(A), "Argument A not in non-decreasing order." # From Chapter 9: # Assume A[0..n-1] is arranged in non-decreasing order. Let k be an # index of A where A[k]==v, or n if no v in A. L: int = 0; R: int = n - 1; k: int # Invariant: v is in A[L..R] if v is in A[0..n-1]. # Variant: R-L. while L != R: M: int = (L + R) // 2 if v <= A[M]: R = M else: L = M + 1 if n != 0 and A[L] == v: k = L else: k = n # return k # 4. Class Specifications. #Uncomment line to run # 1. Statement Specifications. # 1.1. Implementations. #e3_1_1() -> None #e3_1_2() -> None #e3_1_3() -> None # 1.2. Specification Style. #e3_2_1() -> None #e3_2_2() -> None # 1.3. Specifications as Higher-Level Code. #e3_3_1() -> None # 1.4. What? Not how? #e3_4_1() -> None # 1.5. States and Effects. #e3_5_1() -> None #e3_5_2() -> None #e3_5_3() -> None #e3_5_4() -> None #e3_5_5() -> None #e3_5_6() -> None #e3_5_7() -> None # 1.6. Conditions and Sets of States. #e3_6_1() -> None # 1.7. Assertions. #e3_7_1() -> None #e3_7_2() -> None #e3_7_3() -> None #e3_7_4() -> None # 2. Declaration Assertions. # 3. Method Specifications. #e3_8_1() -> None # 4. Class Specifications.