contracts with logilab.aspects

Syntax :

The contracts are read in docstrings since they can be considered as part of the documentation. The part of the docstring which holds contract definitions is divided in three parts : pre, post, and inv. These three parts must be grouped together in the docstring. Each part looks like:

separator:
condition1
condition2
...
conditionN

where separator can either be pre, post or inv according to what type of condition you want to describe. The conditions are Python boolean expressions.

Example:

def push(self, obj):
    """
    pre:
        obj is not None
        not self.is_full()
    post:
        not self.is_empty()
        self.top() == obj
    """
    raise NotImplementedError

Here, preconditions are : obj is not None and not self.is_empty(), postconditions are : not self.is_empty() and self.top() == obj.

Key words:

The key words that can be used in contracts are :

• __return__ : the value returned by the wrapped method. (This is only a keyword in postconditions.)

• __old__ : which allows you to use the state of a variable at the beginning of the method. __old__ can only be used in post-conditions. As an example, we can write a post-condition which will check that a stack's size has been incremented after a push() call. This can be done by writing :

  """
      post:
          self.size() == __old__.self.size() + 1
      """
  

• forall(sequence, mapped_func) which will check that applying mapped_func on all elements of the sequence will give a "True" result. If no "mapped_func" is given, then all the sequence elements must be 'True' for forall to return "True". In the following example, we will test that a list is well sorted (code adapted from pycontract, http://www.wayforward.net/pycontract/pep-contract.html) :

  def sort(self, array):
  """
  post:
      # array size is unchanged
      len(array) == len(__old__.array)
  
      # array is ordered
      forall([array[i] >= array[i-1] for i in range(1, len(array))])
  """
  array.sort()
  

• exists(sequence, mapped_func) which is the same as forall, but only one element has to conatin a 'True' result for exists to return True.

The code for forall and exists has been taken from http://www.wayforward.net/pycontract/pep-contract.html which defines a way to implements contracts in Python.

Inheritance:

The inheritance rules are the following ones :

• pre-conditions can only be kept or weakened through inheritance. Otherwise, it's a contract violation. As a consequence, pre-conditions in a sub-class are ORed with pre-conditions in base classes.
• post-conditions can only be kept or strengthened, otherwise it's a contract violation. As a consequence, post-conditions in a sub-class are ANDed with post-conditions in base classes.
• The same rules are applied for invariants and post-conditions

Exception management:

If an exception is raised in the wrapped method, then post-conditions are not tested, but invariants are.