Pre and Post Conditions in Python

Pre and post conditions are a fundamental aspect of software development that help ensure the correctness and reliability of code.
In Python, we can use :

• assertions to implement pre and post conditions effectively,

• type hints via typechecking tools to enforce type constraints and improve code readability

Docstrings should be used to document the pre and post conditions of functions, providing clear guidance to developers on how to use the functions correctly and what to expect from them.
Sometimes checking pre and post conditions can be computationally expensive, so it’s important to consider the performance implications when implementing them, especially in performance-critical code.
Therefore it’s a good practice to use assertions for pre and post conditions during development and testing, and to disable them in production environments to avoid unnecessary overhead.
Therefore it can be beneficial to use systems that enable to selectively enable or disable pre and post condition checks based on the environment or configuration, allowing for a balance between safety and performance.

In anycase, tests should be implemented to verify that the pre and post conditions are correctly defined and that the functions behave as expected when those conditions are met or violated.

To document properly those elements, we use the PEP 316 - Programming by Contract for Python from Ternece Way https://peps.python.org/pep-0316/ and the PEP 484 – Type Hints by Guido van Rossum, Jukka Lehtosalo, and Łukasz Langa https://www.python.org/dev/peps/pep-0484/#type-hints

In restructured text, we document invariants, preconditions and postconditions using the following syntax:

def function_name(parameter_1: type, parameter_2: type) -> return_type:
     """Function description.

     :inv:
         invariant_1
         invariant_2
         ...
     :pre:
         precondition_1
         precondition_2
         ...
     :post:
         postcondition_1
         postcondition_2
         ...

      # or if the post conditions are related to the state of the object itself, we can use :post[self]: instead of :post: to indicate that the post conditions refer to the state of the object after the function execution.
      :post[self]:
         postcondition_1
         postcondition_2
         ...

      Parameters
      ----------
      parameter_1 : type
          Description of parameter_1.
      parameter_2 : type
          Description of parameter_2.

      Returns
      -------
      return_type
          Description of the return value.

      Raises
      ------
      ExceptionType
          Description of the exception that may be raised.
     """