===============================
Contract specific documentation
===============================

Contracts are here defined as aspects. Contract activation is be done
by weaving ContractApsect code.

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 adpated 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 that *forall*, but
      only one element should give 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 are *ORed* with base classes ones.
    - *post-conditions* can only be **kept** or **strengthened**,
      otherwise it's a contract violation. As a consequence,
      post-conditions are "ANDed" with base classes ones.  
    - 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.

