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

Contracts are here defined as aspects. Contract activation is being 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 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.

