What is a postcondition? Definition and examples

When designing and implementing an application, ensuring its correctness is a crucial concern. One of the approaches you can use to achieve that is making sure the modules of your application communicate clearly with one another, expressing their expectations and guarantees to each other in a clear way.

Postconditions are one of the techniques you can use to ensure your modules express their intents and guarantees to their callers, contributing to more manageable code.

Correctness is the prime quality. If a system does not do what it is supposed to do, everything else about it—whether it is fast, has a nice user interface—matters little.

– Bertrand Meyer, in Object-Oriented Software Construction

In this guide, we introduce the concept of postconditions: their meaning, their use cases, how they relate to other concepts, the role they play in programming, and more.

What is a post condition?

Definition

A postcondition is a “guarantee” that a software function makes to its callers. The specific mechanism you can use to express that guarantee varies across languages, but the general principle is the same: a function somehow expresses that a given condition will be true by the time it returns.

That means that a caller can assume that the result of the function will be valid and safe to use.

What is the difference between a precondition and a postcondition?

Postconditions are related to preconditions, in the sense that they are conceptually opposite. A postcondition is a guarantee that a function makes to its callers, in the form of verifying that one or more conditions are true before it returns. A precondition, on the other hand, is a requirement a function makes of its callers, by demanding some conditions be true before it does any work.

The role of postconditions in programming

After briefly covering the definition of postconditions, it’s time to explain more in depth about the roles they play in coding.

As we’ve just covered, postconditions are supposed to help in program correctness, but how do they do that in practice? What is the problem they help solve?

Explaining the problem

In an application, modules communicate with each other. A given function A might call function B, which then calls C and D. Each one of these functions accepts parameters and returns some value as well, which then poses the question: Whose responsibility is it to ensure the correctness of the values a function needs to work?

The function itself? Its callers?

A proposed solution to this issue is the concept of design by contract.

How do postconditions relate to contract-based programming?

Design by contract, also called contract-based programming, among other names, is an approach to software design created by Bertrand Meyer.

The main idea is that software modules—objects, methods—can create contracts between them, in the same way that people do, defining the obligations and expectations of each one, so they all work together efficiently.

Postconditions are one of the three “pillars” of contract-based programming, as Mark Seemann puts it:

Contracts, according to Meyer, describe three properties of objects:

• Preconditions: What client code must fulfil in order to successfully interact with the object.
• Invariants: Statements about the object that are always true.
• Postconditions: Statements that are guaranteed to be true after a successful interaction between client code and object.
  – Mark Seemann, “Stubs and mocks break encapsulation”

Why are postconditions important in ensuring program correctness?

If the caller of a function can safely assume it will get a valid, correct answer, then it doesn’t need to check the integrity of that result. This leads to code that is less prone to errors but also generates code that doesn’t need to be overly defensive, resulting in a cleaner design, which leads to better maintainability.

What is an example of a postcondition?

Imagine a list class that has an add or append method that, when called, adds the specified item to the end of the list.

Here are examples of postconditions for such a method:

• By the end of the method, the length of the list must have increased by one
• By the end of the method, the last element in the list must be the specified item

How do postconditions work in practice? The answer depends on which language we’re talking about.

How are postconditions specified?

Up until now, we’ve covered postconditions in a more high-level way. But how do they work in practice? The answer depends on which language we’re talking about.

Bertrand Meyer is the creator of the Eiffel programming language and, as such, this language has native support for contract-based programming, which includes postconditions. Support in other languages can be added via libraries, frameworks, assertions, exceptions, or even via documentation (e.g., comments).

Examples of postconditions

Earlier, we talked about a postcondition example for a list method that enabled users to add a new element. Examples of postconditions were to verify whether the list size increased by one and verify whether the list’s last element was the same as the specified value.

The following is an example of how this could be implemented in C#:

public class IntList
{
    private List<int> _innerList = new();

    public void Add(int x)
    {
    	var initialCount = _innerList.Count;
    	_innerList.Add(x);
    	var finalCount = _innerList.Count;

    	if (finalCount != initialCount + 1)
        	throw new Exception("Postcondition failed: final count isn't initial count + 1!");

    	if (_innerList[^1] != x)
        	throw new Exception("Postcondition failed: last element isn't expected.");
    }
}

But it could be argued that those conditions are never supposed to be false during runtime. So, for postconditions that are only meant to be checked during development and debug time, it probably makes more sense to use assertions:

public class IntList
{
    private List<int> _innerList = new();

    public void Add(int x)
    {
    	var initialCount = _innerList.Count;
    	_innerList.Add(x);
    	var finalCount = _innerList.Count;

    	Debug.Assert(finalCount == initialCount + 1, "final count isn't initial count + 1!");
    	Debug.Assert(_innerList[^1] == x, "Postcondition failed: last element isn't expected.");
    }
}

Here’s the translation of the same code, but now in Python:

class IntList:
    def __init__(self):
    	self._inner_list = []
    
    def add(self, x):
    	"""
    	Add an integer to the list.
   	 
    	Post-conditions:
    	- The size increases by exactly 1
    	- The last element is the added element
    	"""

    	initial_count = len(self._inner_list) 	 

    	self._inner_list.append(x)
   	 
    	# Post-conditions verification
    	final_count = len(self._inner_list)
    	assert final_count == initial_count + 1, "Post-condition failed: final count isn't initial count + 1"
    	assert self._inner_list[-1] == x, "Post-condition failed: last element isn't expected"

Finally, let’s see the same example in JavaScript:

class IntList {
constructor() {
this._innerList = [];
}

add(x) {
const initialCount = this._innerList.length;
this._innerList.push(x);
const finalCount = this._innerList.length;

console.assert(finalCount === initialCount + 1, "final count isn't initial count + 1!");
console.assert(this._innerList[this._innerList.length - 1] === x, "Postcondition failed: last element isn't expected.");
}
}

How are postconditions tested?

Since postconditions are such valuable programming constructs, it makes sense that you’d like to test your postconditions as part of your automated test suite. How to go about that?

There isn’t much mystery about testing postconditions—or preconditions, for that matter. You’d just write those tests as part of your regular unit tests. Specifically for postconditions, you can write tests that verify:

• Whether return objects are in a valid state
• Whether exceptions haven’t been thrown
• If the object in general is in the expected state
• If expected exceptions have been thrown—in the case of test cases that verify the error path instead of the happy path

Together, preconditions, invariants, and postconditions are the main pillars of contract-based programming.

Conclusion

Postconditions are a way for functions to express guarantees they make—about their state, the state of their overall object, or another piece of data. That way, other functions “know what to expect” and play efficiently together, resulting in code with more stability and correctness.

The opposite of postconditions are preconditions, which are the requirements a function makes to its callers. Finally, invariants—which we haven’t covered in this article—refer to facts or predicates about an object’s state that must remain true for the whole duration of that object’s life.

Together, preconditions, invariants, and postconditions are the main pillars of contract-based programming, an approach pioneered by Bertrand Meyer with the ultimate goal of enabling the creation of object-oriented software with high degrees of robustness and correctness.

This post was written by Carlos Schults. Carlos is a skilled software engineer and an accomplished technical writer for various clients. His passion is to get to the bottom (the original source) of things and captivate readers with approachable and informative technical content.