Master d’informatique 2006 2007 de l’université Paris VI
cps
Langage de description des contrats

Introduction

Voici les constructeurs principaux du langage de spécification des contrats sous la forme d’assertions logiques en commentaires dans les interfaces Java. Ce langage est une version largement simplifié de ce que l’on trouve dans JML ou Spec#

La description du langage est informelle. Il faudrait normalement partir d’une spécification algébrique de type ADT.

Les mots-réservés du langage sont préfixés par un anti-slash \

Exemple

Voici un exemple simple de spécification pour une interface de minuteur :

public interface Minuteur {
 /* Invariant:
  * \inv  getCompte()>=0  : le compte doit être positif
  * \inv  getCompte()<=getDepart() : le compte courant est inférieur au compte des minutes
  * \inv  isTermine()==(getCompte()==0) : le minuteur est terminé quand le compte est nul
  */

 /* Constructeur:
  * \pre minutes>0 : on compte au moins une minute
  * \post getCompte()==minutes
  * \post getDepart()==minutes
  */
  public void init(int minutes);

 /* Observateurs */
 public int getCompte();
 public int getDepart();
 public boolean isTermine();

 /* Operations */
 
 /** Tick d'horloge
  * \pre !isTermine() : pas de tick possible si minuteur terminé
  * \post getCompte() == getCompte()@pre - 1
  * \post getDepart() == getDepart()@pre
  */
 public void tick();
}

Assertions logiques java

On peut tout d’abord décrire des assertions logiques sous la forme d’expression booléennes comme on le ferait dans du code Java.

- égalité référentielle : ==
- ou logique ||
- et logique &&
- non logique ! !

Invocation des observateurs

Les observateurs de l’ADT sont bien sûr utilisables

ex. getCompte()

Dans les post-conditions,on peut également invoquer les observateurs "au moment de la précondition"

ex. getCompte()@pre

Les observateurs externes d’autres ADT peuvent être invoqués. Dans les post-conditions, cependant, on ne peut pas les invoquer avec @pre

ex. getCompte(getDernierCompteCree()).solde() (ADT des comptes bancaires)

Finalement, tout accesseur Java peut être invoqué (toujours sans @pre) :

ex. getActivePrios().isEmpty()      // interface Set<Integer> ex. obj1.equals(obj2)  // égalité structurelle

Remarque : normalement il ne faut aucun effet de bord, un outil devrait le vérifier

Paramètres

Les paramètres des méthodes sont également observables dans les préconditions et postconditions :

ex. minutes (paramètre minutes du constructeur)

Quantificateurs

Les quantificateurs de logique des prédicats (ordre 1) sont disponibles avec la syntaxe suivante :

On peut également utiliser des intervalles pour les collections :

Ensembles par compréhension

On ajoute une syntaxe pour pouvoir décrire des ensembles par compréhension :

syntaxe : \{expr(X) \suchthat X:Type \in Collec \} avec expr une expression quelconque, fonction de X. Si l’expression est du type T, on retourne un ensemble du type Set<T>

exemple :

\sum \{ getSizePrio(prio) \suchthat prio:Integer \in getActivePrios() \} == 0

Une possibilité supplémentaire est de filtrer les éléments avec une propriété :

syntaxe 2 : \{ obs(X) \suchthat X:Type \in Collec \if prop(X) \}

exemple :

\sum \{ getSizePrio(prio) \suchthat prio:Integer \in getActivePrios() \if \even(prio) \} == 0

Si nécessaire, on peut supposer l’existence de fonctions utilitaires :

Exemple :

\max : Number * Number -> boolean
\min : Number * Number -> boolean
\sum : Collection<T extends Number> -> int

Retour à la page d’accueil