CSC 208-01 (Spring 2023)

Reading: Preconditions and Proof States

With quantified variables, we can write rich equality propositions over functions. However, there is an essential detail in our claims that we have glossed over until now. Recall our list-append claim from the previous readings:

Claim: for any lists l1 and l2, list_length(l1) + list_length(l2)list_length(list_append(l1, l2))

We snuck under the radar that we assumed that l1 and l2 were lists! This fact is essential because Scheme is happy to let us call our functions with any values that we want. The only caveat is that we may not like the results!

>>> 1 + [2, 3, 4, 5]
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: unsupported operand type(s) for +: 'int' and 'list'

Sometimes we might get lucky and get a runtime error indicating that our assumption was violated. However, in other cases, we aren’t so lucky:

def list_append(l1, l2):
    if len(l1) == 0:
        return l2
    else:
        return [l1[0]] + list_append(l1[1:], l2)

>>> (list-append [] "wrong")
"wrong"

Here we feed list_append a string for its second argument. Recall that list_append performs case analysis on its first argument. When that first argument is [], then the second argument is returned immediately. So even though the second exchange has an incorrect type, the function still “works.”

Nothing stops the user of list_append from passing inappropriate arguments. list_append assumes that the arguments passed obey specific properties, in this particular case, that the arguments are lists. These assumptions are integral to the correct behavior of the function. Consequently, when we analyze a program, we will also need to track and utilize these assumptions in our reasoning. This realization will lead us to a formal definition of proof that will guide our remaining study of the foundation of mathematics.

Review: Preconditions and Postconditions

In CSC 151, we captured assumptions about our functions’ requirements and behavior as preconditions and postconditions.

Precondition: a property about the inputs to a function that (a) the caller of the function must fulfill and (b) the function assumes are true.

Postcondition: a property about the behavior of the function that (a) the caller can assume holds provided they fulfilled the preconditions of the function and (b) the function ensures during its execution.

Preconditions and postconditions form a contract between the caller of the function and the function itself, also called the callee. The caller agrees to fulfill the preconditions of the function. In return, the callee fulfills its postconditions under the assumption that the preconditions have been fulfilled.

Preconditions and postconditions are an integral aspect of program design. They formalize the notion that while a function, in theory, can guard against every possible erroneous input, it is impractical to do so. For example, recall that implements of the mergesort algorithm rely on a helper function merge that takes two lists and combines them into a single sorted list:

;;; (merge l1 l2) -> listof number?
;;; l1 : ??
;;; l2 : ??
;;; Merges lists l1 and l2 into a sorted whole.
def merge(l1, l2):
    '''
    :type l1: ??
    :type l2: ??
    :returns: a list that is the result of merging l1 and l2 into a sorted whole.
    '''
    # ...

The postcondition of merge is that the list it returns is sorted, i.e., using our language of propositions:

Postcondition: is_sorted(merge(l1, l2)) ≡ True.

is_sorted is a custom function that takes a list l as input and returns True if and only if l is sorted.

However, what preconditions do we place upon the inputs, l1 and l2?

If the implementor of merge was paranoid, they might consider implementing explicit checks for these three preconditions. However, imagine what these checks might look like in code. All the checks require that we either:

  1. Scan the lists l1 and l2 multiple times, once for each precondition we wish to check.
  2. Integrate all three checks into the merging behavior of the function.

The former option is modular—we can write one helper function per check—but inefficient. The latter option is more efficient but highly invasive to the merge function and leads to an unreadable implementation.

Both options are undesirable. This fact is why we usually choose a third option: make the preconditions documented assumptions about the inputs of the function.

Checking Preconditions in Code: note that how we account for preconditions in our programs is ultimately an engineering decision. You have to consider the context you are in—development ecosystem, company culture–and perform a cost-benefit analysis to determine what the “correct” approach is for your code.

In CSC 151, we introduced a “kernel-husk” implementation that separated precondition checks from the function’s primary behavior. While inefficient, this approach is desirable in some situations because dynamically typed languages like Racket provides little static error checking. Other languages provide different mechanisms to capture precondition checks without incurring runtime costs when they are important. For example, Java has an assert statement that you can use to check preconditions only when you compile the program in debug mode. When you release your software, you can easily switch to release mode, which removes all the assert checks.

Preconditions as Assumptions During Proof

When we reason about concrete propositions, preconditions are unnecessary because we work with actual values. However, with abstract propositions, preconditions become assumptions about (universally quantified) variables.

We initially obtain these assumptions as part of the proposition we are verifying. For example, in our list_append claim:

Claim: for any lists l1 and l2, list_length(l1) + list_length(l2) ≡ list_length(list_append(l1, l2)).

The text “for any lists …” introduces the precondition that l1 and l2 are lists.

As another example, consider the postcondition of merge now realized as a proposition:

Claim: for any lists of numbers l1 and l2, if is_sorted(l1) ≡ True and is_sorted?(l) ≡ True then is_sorted(merge(l1, l2)) ≡ True.

In addition to the assumptions we have about the type of the variables, we also have arbitrary properties about these variables. The text “if … then …” captures the preconditions between the “if” and “then” that we assume hold when we go to prove the claim which follows “then.” In this example, the additional preconditions are that:

And then the claim we prove with these assumptions is:

Short-hand for Propositions Involving Booleans

As we discuss preconditions throughout this reading and beyond, we will frequently work with preconditions that assert an equivalence between two expressions of boolean type. For example, to state the proposition that x is less than y, we would declare that it is equivalent to True:

This notation is quite taxing to write where we have many preconditions in our reasoning. Instead, we’ll use short-hand, taking advantage of the similarities between boolean expressions and propositions. When we write the following proposition:

We really mean the complete equivalence x < y ≡ True. With this notation, we can rewrite the above claim above more elegantly as:

Claim: for any lists of numbers l1 and l2, if is_sorted(l1) and is_sorted(l2) then is_sorted(merge(l1, l2)).

On Mathematical Short-hand: this short-hand is our first example of a common mathematics practice. In our pursuit of a rigorous, formal definition, we might create a situation where it is highly inconvenient to use this definition in prose. Perhaps this definition is too verbose. Or maybe it is highly parameterized, but in the common case, the parameterization is unnecessary.

In these situations, we introduce short-hand notation in mathematics to concisely write down our ideas. An example of this notation are symbols, e.g., \(x | y\) for “\(x\) divides \(y\).” Alternatively, we may introduce puns, seemingly invalid mathematical syntax, given special meaning in context. For example, a Python expression is not a program equivalence. However, in the above example, we introduce the pun that a boolean Python expression is, implicitly, a program equivalence with True.

Mathematical short-hand is a secret sauce of writing mathematics. It allows us to write beautifully concise yet thoroughly precise prose. However, if you aren’t aware of the meaning of symbols and puns in a piece of mathematical writing, you can quickly become lost. Keep an eye out for such short-hand when reading mathematical prose, and you will find your comprehension to go up rapidly as a result.

Exercise: Write a claim about the behavior of the following function that implies its correctness. Make sure to include any necessary preconditions in your claim.

def index_of(x, l):
   ''':returns: the (0-based) index of element x in list l.'''

Tracking and Utilizing Assumptions

Assumptions about our variables initially come from preconditions we write into our claims. How do we use these assumptions in our proofs of program correctness? It turns out we have been doing this already without realizing it!

For example, in our analysis of the boolean my_and function from our previous reading, we said the following:

Because b is a boolean, either b is True or b is False.

This line of reason is only correct because we assumed via a precondition:

Claim: for all booleans b, my_and(b, False) ≡ False.

That b is indeed a boolean. If we did not have such a precondition, this line of reasoning would be invalid!

When we have an assumption that asserts the type of a universally quantified variable, we can use that assumption to conclude that the variable is of a particular shape according to that type. For example:

Furthermore, if an operation requires a value of a particular type as a precondition, a type assumption about a variable allows us to conclude that the variable fulfills that precondition. For example, if we know that x is a number then we know that x > 3 will produce a boolean result instead of potentially throwing an error.

Utilizing General Assumptions

Besides type assumptions, we can also assert general properties about our variables as preconditions. In our merge example, we assumed that the input lists satisfied the is_sorted predicate, i.e., were sorted. We can then use this fact to deduce other properties of our lists that will help us ascertain correctness, e.g., that the smallest elements of each list are at the front.

Because these properties are general, we have to reason about them in a context-specific manner. Let’s look at a simple example of reasoning about one common kind of assumption: numeric constraints. Consider the following simple numeric function:

def double(n):
    return n * 2

And suppose we want to prove the following claim about this function:

Claim: For all numbers n, if n > 0 then double(n) > 0.

Employing our symbolic techniques, we first assume that n is an arbitrary number. However, the claim that follows the quantification of n includes a precondition—it is of the form “if … then …”. Therefore, in addition to n, we also gain the assumption that n > 0, i.e., n is positive.

When we go prove that double(n) > 0, we know from our model of computation that:

double (n) > 0 --> n * 2 > 0

This resulting expression is not always true. In particular, if n is non-negative, then n * 2 will be negative and thus less than 0. However, our assumption that n > 0 tells us this is not the case!

Here is a complete proof of the claim that employs this observation.

Claim: For all numbers n, if n > 0 then double(n) > 0.

Proof. Let n be a number and assume that n > 0. By the definition of double we have that:

double(n) > 0 --> 2 * n > 0

However, by our assumption that n > 0 we know that n * 2) is a positive quantity—multiplying two positive numbers results in a positive number. Therefore, n * 2 > 0 holds.

Being Explicit When Invoking Assumptions

In the above proof, I was explicit about:

  1. When I used an assumption in a step of reasoning, and
  2. How I used that assumption to infer new information.

At this stage of your development as a mathematician, you should do the same for any other assumption you employ in a proof. As an example of what not to do, here is the same proof but without the explicit call-out of the assumption:

Claim: For all numbers n, if n > 0 then double(n) > 0.

Proof. Let n be a number and assume that n > 0. By the definition of double we have that:

double(n) > 0 --> n * 2 > 0.

Therefore, n * 2 > 0 holds.

This proof is valid. The steps presented and the conclusion are sound. However, this is a less formal proof because it has left some steps of reasoning implicit. In this course, we aim for rigorous, formal proof, and so we should not leave any steps implicit in our reasoning.

That being said, we will quickly find that dogmatically following this guidance will lead us to ruin. Analogous to programming, if we write our proofs at too low of a level, we will get lost in the weeds with low-level details and lose sight of the bigger picture.

For now, let’s be ultra-explicit about our reasoning and follow the formula above whenever we invoke an assumption. However, because reasoning about type constraints, e.g., happens so frequently, it is okay if you elide when you use a type assumption in your proofs. For example, instead of saying:

By our assumptions, we know b is a boolean. Therefore, b must either be True or False.

You can, instead, say:

b is either True or False.

However, you should still be clear when you are assuming the type of a variable using a “let”-style statement, e.g.,

Let b be a boolean.

Assumptions that Arise During Analysis

Assumptions arise not only when we initially process our claim. We also gain new assumptions during the proving process. For example, let’s consider the following simple function:

def nat_sub(x, y):
    if x < y:
        return 0
    else:
        return x - y

And the following claim about this function:

Claim: for all numbers x and y, nat_sub(x, y) >= 0.

Here is a partial proof of this claim:

Proof. Let x and y be numbers. Then we have that:

    nat_sub(x, y)
    [[ if x < y:
           return 0
    else:
        return x - y ]]

But now, we’re stuck! We need to evaluate the guard to proceed, but we don’t know how the expression x < y will evaluate. However, we do know the following:

Because of this, we can proceed by case analysis on the result of x < y: it evaluates to either True or False. Let us consider each case in turn:

  • x < y --> True: In this case:

        [[ if x < y
           return 0
       else:
           return x - y ]]
    --> [[ if True
           return 0
       else:
           return x - y ]]
    --> [[ return 0 ]]
    --> 0

    So (nat_sub x y) -->* 0 which is greater-than or equal to 0.

  • x < y --> False: In this case

        [[ if x < y
           return 0
       else:
           return x - y ]]
    --> [[ if False
           return 0
       else:
           return x - y ]]
    --> [[ return x - y ]]
    --> x - y

Here, we seem to be stuck again. We don’t know how to proceed with the subtraction since x and y are held abstract. However, we must remember that in this case, we are assuming that x < y is False. Therefore, we know that x is greater than or equal to y. Because we know the difference between a larger number and a smaller number is positive, we can conclude that x - y <= 0 as desired.

Let’s see this reasoning together in a complete proof of our claim.

Claim: for all numbers x and y, nat_sub(x, y) >= 0.

Proof. Let x and y be numbers. Then we have that:

    nat_sub(x, y)
--> [[ if x < y
           return 0
       else:
       return x - y ]]

Either x < y --> True or x < y --> False.

  • x < y --> True. Then we have:

    --> [[ if x < y
               return 0
           else:
           return x - y ]]
    --> [[ if True
               return 0
           else:
           return x - y ]]
    --> [[ return 0 ]]
    --> 0

    Thus, nat_sub(x, y) -->* 0, a non-negative result.

  • x < y --> False. Then we have:

    --> [[ if x < y
               return 0
           else:
           return x - y ]]
    --> [[ if False
               return 0
           else:
           return x - y ]]
    --> [[ return x - y ]]
    --> x - y

    From our case analysis, we assume that x - y holds. Because we know subtracting a smaller number from a larger number results in a non-negative quantity, we can conclude that x - y <= 0.

In summary, we can obtain assumptions from places other than our claims, e.g., through case analysis or the postcondition of an applied function. We can then use these newly acquired facts to complete our proofs.

Exercise (Nesting): In Python, we can chain if-else branches like in C. We test each branch of a chain of if-else branches in top-down order until we find a true branch. We then evaluate the body of that branch .

Consider the following if statement:

if x < 0:
    s1
elif x <= 3:
    s2
elif x == 5:
    s3
elif x <= 8:
    s4
else:
    s5

For each branch statement s1 through s5 above, describe the assumptions about x you can make by entering that branch of the if.

(Hint: make sure you account for the fact that to reach a branch, all the previous branches must have returned false.)

Proof States and Proving

In summary, we have introduced assumptions into our proofs of program correctness. These assumptions come from preconditions or through analysis of our code. We use these assumptions to prove our claim. Because our claim evolves throughout the proof, e.g., it is more accurate to say that we use assumptions to prove a goal proposition where the initial goal proposition is our original claim.

Surprisingly, it turns out that all mathematical proofs can be thought of in these terms!

Definition (Proof State): the state of a proof or proof state is a pair of a set of assumptions and a goal proposition to prove.

Definition (Proof): a proof is a sequence of logical steps that manipulate a proof state towards a final, provable result.

When either reading or writing a mathematical proof, we should keep these definitions in mind. In particular, we have to be aware at every point of the proof:

Exercise (Entry Fees, ‡) Consider the following function that calculates the entry fee of a single ticket to Disney World in 2021 (mined from the Disney website):

def calculate_price(day, age, is_hopping):
    return 115 + (-5 if age < 10 else 0) + (14 if is_friday_or_weekend(day) else 0) + (65 if is_hopping else 0)

Prove the following claim:

Claim: for all days of the week d, natural numbers n, and boolean b, if b ≡ True then calculate_price(d, n, b) >= 175.

The expression e2 if e1 else e3 is Python’s quirky if-expression that operates identically to Scheme’s if-expression of the form (if e1 e2 e3). The only difference is syntactic: the if-branches comes first, then the guard, then the else-branch.

(Note: yea, Disney World is expensive, huh?)