=====================================
Documentation spcifique aux contrats
=====================================


Les contrats sont ici dfinis comme des aspects. Activer les contrats
revient donc  tisser l'aspect "contrat" dans le code souhait.

Syntaxe :
---------

Les contrats sont lus dans les **docstrings** des mthodes Python.
La partie de la *docstring* qui est consacre  dcrire les contrats se
divise en trois parties : **pre**, **post**, et **inv**. Ces trois parties
doivent **IMPRATIVEMENT** se suivre dans la *docstring*. Chacune de ces
parties est de la forme :

::

	delimiteur:
        condition1
        condition2
	    ...
	    conditionN

o le *delimiteur* est **pre**, **post** ou **inv** suivant
que l'on veuille dcrire respectivement une pr-condition, une post-condition
ou un invariant. La syntaxe des conditions est directement la syntaxe
de Python.

:Exemple:

::

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

Ici, les prconditions sont : *obj is not None* et *not self.is_empty()*. Les
postconditions sont : *not self.is_empty()* et *self.top() == obj*.


:Mots cls:

Les mots-cls qui peuvent tre utiliss dans les contrats sont :

- **__return__** : la valeur de retour de la mthode (uniquement dans les
  post-conditions).
- **__old__** : pour avoir accs  l'tat d'une variable telle qu'elle tait
   l'entre de la fonction. **__old__** ne s'utilise donc uniquement que
  dans les post-conditions. Les variables que l'on peut dsigner avec
  **__old__** sont les variables passes en paramtres de la mthode ou
  *self*. En thorie, il est en fait possible d'accder avec *__old__*  toutes
  les variables auxquelles on pourrait avoir accs  la premir ligne
  de la mthode wrappe.
  Un exemple d'utilisation de **__old__** : on pourrait trs bien dans la
  mthode *push()* d'une classe d'implmentation d'une *Pile* vouloir
  s'assurer, dans les post-conditions que la taille de la pile a bien
  t incrmente de 1. C'est possible en crivant : ::

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


- **forall(sequence, mapped_func)** qui vrifie que l'application de
  mapped_func sur tous les lments de la squence donne un rsultat
  vrai. Si mapped_func n'est pas prcis, alors tous les lments de
  la squence doivent tre vrai.
  Dans l'exemple suivant, on va vrifier que le tableau est bien
  tri  la fin de la mthode sort(). (code adapt de *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)** : idem que *forall()* mais un seul
  des lments de la liste doit tre vrai.


Le code de *forall* et *exists* a t pris dans le projet :
*http://www.wayforward.net/pycontract/pep-contract.html* qui dfinit
une manire d'implmenter les contrats en Python.

:Hritage:

Les rgles concernant l'hritage de contrats sont les suivantes :

- Les *pr-conditions* ne peuvent tre renforces dans une sous-classe.
  Elles peuvent uniquement tre **conserves** ou **affaiblies**, sinon
  c'est une violation de contrat. Par consquent, on applique un *OU*
  entre les pr-conditions d'une mthode et celles de la mme mthode dans
  les classes-mres.
- Les *post-conditions* ne peuvent pas tre affaiblies. Elles sont donc
  soit **conserves** soit **renforces**, sinon, c'est une violation de
  contrat. Par consquent, on applique un *ET* entre les pr-conditions
  d'une mthode et celles de la mme mthode dans les classes-mres.
- Les *invariants* appliquent les mmes rgles que pour les *post-conditions*.


:Gestion des exceptions:

Si une exception est leve par la mthode wrappe, alors les post-conditions
ne sont pas prises en compte. En revanche, les invariants sont toujours
vrifis.
Pour le reste, les "contrats" tant gr comme des aspects,
la gestion des exceptions se fait de la mme manire.

