=====================================
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.

