A function’s precondition refers to what must hold before the function is executed, and a function’s postcondition refers to what will be true or changed after the execution of the function in addition to what it returns.

If the function modifies a global variable, for example, this variable’s state should be included in the preconditions. A tremendous number of bugs occur due to incomplete understanding of preconditions and postconditions of a function.

For instance, if you pass a negative integer to a function that handles only positive integers, you get weird results or even a exception error.

Another example is that if the result of calling a function is further processed by the program, you need to make sure the program can deal with every single possible result the function returns. That is why if you do not pay enough attention to a function’s preconditions and postconditions, it is highly possible that your function works on some arguments and crashes on others.

Let me give you an actual coding example. Consider the following function:

int get_sum(int first_int, int second_int, int &sum){
  sum = first_int + second_int;
  return sum;
}

This function computes the sum of the two given integers and stores it in the given argument sum as well as returning it. In this case the precondition is that first_int and second_int are valid integers bound by C++’s integer maximum value and minimum value. And the postcondition is that the sum of those integers is returned and variable sum is updated to store the value of the sum.

Knowing exactly the state of the program before and after the execution of a function is extremely important. It will greatly reduce logic errors and confusion.

Preconditions

Preconditions are conditions that must be true prior to running a method.

Each method will have its own precondition. These conditions can apply to one of two things: data members or parameters. Typically, they apply to parameters.

For example, you might have a BankAccount object and a depositMoney() method. The depositMoney() method would, presumably, take an argument indicating the amount of money to be deposited, and that money should be positive. So, a precondition would be money > 0.

If the person calling the method fails to observe the precondition, by passing in a negative argument, the depositMoney() may actually cause the account to become negative. This is actually OK, because that's the purpose of the precondition. It's a warning to the caller of the method to follow the precondition, and if the caller fails to heed the warning, then the object will (potentially) be corrupted.

Or, if you have withdrawMoney() method, the precondition may affect both the parameter (e.g., money > 0) and the data member (e.g., balance > 0).

You might, however, make a precondition for a method to be "true". This means, you place no restrictions on the input or the data members. Again, consider depositMoney(). You could allow the user to send in money that's negative. If negative, nothing is done (since it wouldn't make sense).

Postconditions

Where preconditions serve to let the caller of a method know when it's safe to call a method, postconditions let the caller of a method know what happens after the method has completed calling. Usually, postconditions are harder to specify.

The purpose of a postcondition is threefold:

• to indicate how the data members have changed.
• to indicate how the parameters passed in have changed.
• to indicate what the value of the return type is.

In a nutshell, the postconditions tell you what happened after calling the method. The reason it's difficult to specify a postcondition is that it can be difficult to describe the underlying data structure.

For example, if you have a linked list, how do you describe it, so that it reflects the nature of the linked list? The answer is often: you don't. You may have to come up with some math notation that describes the essentials of what is happening.

Here's an example. For an unsorted list, you might add an element to the front of back. So, we can write the following: list = elt + list', where + is basically a concatentation operator, and elt is appended at the front of a list.

There's another reason postconditions are harder to specify. You have to describe what changed. That means, you have to describe what used to be, and what is now.

If you're careful, you may have noticed a quote. Call this mark, "prime". list' (read: list prime) will be the list as it was just as the method was being called. list is the list at the end of the call.

Thus, list = elt + list' means that the new list is the old list with elt attached at front. This becomes even more of a problem to describe for trees.

Ultimately, it's easier to write code to test postconditions than to describe it in English/first order logic.

Example: Stack

Let's look at an example of coding a stack. A stack should support the following operations:

• push() add an element to the top.
• pop() remove an element to the top.
• size() return the number of elements in stack.
• isEmpty() returns true, if stack is empty (size is 0).
• peek returns the top element, without removing it.

Then, we look at the precondition and postconditions of each of the methods.

push( string str )

If a static array is used, then its size would be fixed, and a precondition would have to be that the stack size is smaller than the maximum stack size.

The postcondition is trickier. It requires that we keep track of the size prior to adding, and also the data elements prior to adding. We'll refer to the old size as size' (size prime) and the previous elements as list'.

Thus, the postcondition is that size = size' + 1 and that the list is list' plus the str just added.

Precondition: true or size < max_size_of_the_array
Postcondition: size == size' + 1 AND list == str + list'.

The real difficulty with describing the postcondition is to use some math terminology, which is precise and short, so that we avoid discussing code, which can be verbose. When using math terminology, it can be easy to lose "precision". For example, what does list == str + list' exactly mean?

pop()

The precondition for pop() is a little trickier. Theoretically, you can add as many elements to a stack as you want (in reality, you worry about the amount of memory available). However, you can't remove as many elements as you want. In particular, if the stack is empty, there's no more elements to remove. What should you do?

We can establish that the precondition is size > 0. A precondition is like a warning label. It says that if the precondition is not met, then the operation may fail. This could be as "harmless" as simply not recording the data, to as serious as corrupting data or core dumping.

But suppose you did the following. You tested, within the pop() code if the size was 0, and if not, you returned back a default "error" object (something the user would be able to tell). In that case, the precondition would be "true", because the code actually takes care of the case when the stack is empty. The precondition indicates when you will correctly handle the call, and "true" is more accurate than size > 0.

Precondition: size > 0
Postcondition: size = size' - 1 && result + list == list'.

size()

The precondition and postcondition for size() is both true. size() is a query method. That means, it doesn't modify the data members. Therefore, there's no postcondition. We can leave it as "true". Or you can say "result == size" which indicates what that "size" was returned.

Precondition: true
Postcondition: result == size

isEmpty()

Like size(), there's not really much of a precondition. You can always call this method. The postcondition only applies to the return value, which returns true if size is equal to 0.

Precondition: true
Postcondition: result == ( size == 0 )

peek()

You can only peek when there's something to peek at. The difficult is describing what gets returned as a result.

Precondition: size > 0
Postcondition: result == top of stack