Table des matières

OCL

Invariants

Exemples avec club vidéo

Une vidéo empruntée est nécessairement une vidéo de l’inventaire

context Succursale
inv: self.videos->includesAll(self.clients.videos)

Deux clients distincts ne peuvent avoir des vidéos en commun.

context Succursale
inv: self.clients->forAll(c1, c2 | c1.videos->intersect(c2.videos) implies c1 = c2)

Requêtes

class Person
  attributes
    firstname: String
    lastname: String
    email: Set(String)
  operations
    fullname(prefix:String) : String =
      prefix.concat(' ').concat(firstname).concat(' ').concat(lastname)
end
prefix= 'Mr' ou 'Dr' ou 'Mad.' etc.

Opérations

Syntaxe

context Typename::operationName(param1 : Type1, ...): ReturnType
  pre precondname1 : ...param1... ...self...
  pre precondname2 : ...param1... ...self...
  ...
  post postcondname1 : ...result... ...param1... ...self...
  post postcondname2 : ...result... ...param1... ...self...

Exemple 1

class Cours
  attributes
    titre: String
    sigle: String
  operations
    addPreRequis(c : Cours)
end

class Etudiant < Personne
  operations
    abandonCours(c : Cours)
    nouveauCode(n : String)
end

context Etudiant::abandonCours(c: Cours)
  pre Estinscrit: self.cours->includes(c)
  post Plusinscrit: self.cours = cours@pre->excluding(c)

La partie self.cours = cours@pre->excluding(c) est préférable à self.cours->excludes(c) car il peut arriver qu'après l'opération l'ensemble soit vide par erreur, donc qu'il exclus effectivement c, mais qu'en réalité, l'ensemble ne devait pas être vide et exclure c. @pre permet de faire référence à l'état de cours avant l'opération et de pouvoir comparer les deux états avant et après.

Exemple 2

context A::sort(s : Sequence(Integer)) : Sequence(Integer)
  post MemeTaille:result->size = s->size
  post MemesElements: result->forAll(i | result->count(i) = s->count(i))
  post EstTriee: Sequence{1..( result->size-1)}->forAll(i | result.at(i) <= result.at(i+1))

Notez l’utilisation d’une séquence ici pour imiter une boucle de 1 à result->size-1.

Vérification des pre et post conditions

Types primitifs

Real

Operations
+ (r: Real): Real	abs(): Real	< (r: Real): Boolean
- (r: Real): Real	floor(): Integer	> (r: Real): Boolean
* (r: Real): Real	round(): Integer	<= (r: Real): Boolean
/ (r: Real): Real	max(r: Real): Real	>= (r: Real): Boolean
-: Real	min(r: Real): Real

Integer

Operations
−: Integer ⇒ Valeur négative de `self`.	abs(): Integer
+ (i: Integer): Integer	div(i: Integer): Integer ⇒ Le nombre de fois que `i` entre complètement dans `self`.
- (i: Integer): Integer	mod(i: Integer): Integer ⇒ Modulo
* (i: Integer): Integer	max (i: Integer): Integer
/ (i: Integer): Real	min(i: Integer): Integer

String

Operations
size(): Integer
concat(s: String): String
substring(lower: Integer, upper: Integer): String
toInteger(): Integer
toReal(): Real

Boolean

Operations
or (b: Boolean): Boolean
xor (b: Boolean): Boolean
and (b: Boolean): Boolean
not: Boolean
implies (b: Boolean): Boolean

Types collections

Collection

Set

Bag

Sequence

Outils

Dresden OCL toolkit
EmPowerTec - Vérification de la syntaxe et de la sémantique de base
KeY Project - Vérification formelle, OCL et JML
USE - The UML-based Specification Environment.
Neptune (académique) et Topcased (industriel).
OCLE 2.0 - Object Constraint Language Environment (pas de développement depuis 2005).

Sources

S. Benette, J. Skelton, K. Lunn, 2004. Schaum's Outlines of UML, McGraw Hill.