Cours programmation objet concepts avancés

Cours programmation objet concepts avancés, tutoriel & guide de travaux pratiques en pdf.

La part perdue du développement logiciel

I Un programme informatique est la réalisation exécutable d’une spécification.
I On s’assure qu’un programme n’a pas d’erreur en vérifiant qu’il est conforme à sa spécification.
I Le développement de la spécification devrait avoir autant d’importance que le développement du programme.
⇒ L’absence de spécification précise donne l’illusion qu’un dysfonctionnement du programme n’est pas une erreur de la part du programmeur mais, peut-être, un « léger défaut de conception » . . .

La programmation par « contrat »

I Expliciter la spécification d’un programme permet d’en améliorer la qualité et d’atteindre in fine l’objectif d’un logiciel correct par construction.
I Si on voit un programme comme une fonction mathématique f définie sur un ensemble d’entrées I et produisant des résultats dans un ensemble de sorties S, alors une spécification est un couple de prédicats (P, Q) tels que :
∀i ∈ I, P(i) ⇒ Q(i, f (i))
I P est la précondition, spécifiant le domaine correct d’utilisation.
I Q est la postcondition, spécifiant la relation logique liant l’entrée et la sortie.

Le contrat du pauvre en C++

#include hcasserti
#define check_precondition (P) assert (P)
#define check_postcondition (Q) assert (Q)
// input : t
// precondition : t.size () > 0
// output : x
// postcondition : x ∈ t ∧ ∀a, a ∈ t ⇒ x ≤ a int min (std : : vectorhinti t) {
check_precondition (t.size () i 0) ; int x = t[0] ;
for (int i = 1 ; i h t.size () ; ++i)
x = t[i] < x ? t[i] : x ;
check_postcondition (
exists (t.begin (), t.end (), bind2nd (equalhinti(), x))
&& forall (t.begin (), t.end (), bind2nd (greater_equalhinti(), x))) ;
}

Explication

I La fonction assert permet de tester qu’une condition est vérifiée en un point donné du programme.
I Si elle est invalide, le programme est stoppé en précisant le numéro de ligne de la commande de vérification pour aider au diagnostic.
I On peut désactiver la vérification en passant l’option -DNDEBUG au compilateur.

Déterminer le composant responsable

Première critique :
I Si une erreur de violation de la postcondition est signalée à l’endroit pertinent, ce n’est pas le cas pour une erreur sur la précondition.
I On aimerait qu’une erreur d’utilisation de la fonction soit signalée au niveau de l’appel de cette fonction.
⇒ Une intégration de ces notions dans le langage permettrait cela.
Une boîte noire, c’est utile . . . mais l’avion a déjà explosé
Seconde critique :
I Vérifier le respect des préconditions et des postconditions durant l’exécution est tardif et ne prouve rien sur les exécutions futures du programme !
I De plus, il n’est pas certain que toute spécification soit exécutable !
I Enfin, un argument logique ou mathématique est parfois nécessaire pour montrer qu’un programme vérifie sa spécification.
⇒ L’utilisation d’un analyseur statique (similaire à un vérificateur de type) serait plus efficace !

Le cours d’aujourd’hui

1. Le langage Eiffel qui est centré sur la programmation par contrat.
2. Les outils de vérification statique pour les langages à objet.

Eiffel

I Eiffel est un langage de programmation objet basé sur des classes.
I Il est développé par Bertrand Meyer depuis 1986.
I Le compilateur SmartEiffel est développé par l’INRIA.
I Eiffel a les propriétés suivantes :
I Il est typé statiquement.
I Son système de type traite les polymorphismes d’inclusion et paramétrique borné. Il a aussi quelques traits « exotiques » (covariances des arguments des méthodes et des paramètres de type . . . ).
I Il intègre de l’héritage multiple, fournit des primitives de renommage.
I Il fournit un équivalent des fonctions de première classe, appelé des agents.
I Son environnement d’exécution inclut un ramasse-miette et est concurrent.
I Les méthodes peuvent être des requêtes (qui ne modifient pas l’objet) ou bien des commandes (qui le modifient).
I L’accès à un attribut d’une instance suit la même syntaxe que l’appel d’une fonction sans argument (similaires aux propriétés de C# ).
⇒ Aujourd’hui : la programmation par contrat en Eiffel.

Une classe, une méthode et son contrat en Eiffel

class MIN
creation {ANY}
default_create
feature {ANY}
is_min (t : ARRAY[INTEGER] ; m : INTEGER) : BOOLEAN is
– … Définition effacée …
min (t : ARRAY[INTEGER]) : INTEGER is
require – Précondition
t.count > 0
local
x : INTEGER
i : INTEGER
do
x : = t.item(0) from
i : = t.lower until
i > t.upper loop
if x > t.item (i) then
x : = t.item (i)
end
i : = i + 1
end
Result : = x
ensure – Postcondition
is_min (t, Result)
end

Contrat pour des objets

I L’environnement d’exécution de Eiffel est équipé pour fournir des rapports d’erreur permettant de déterminer si une erreur provient de la façon dont on appelle une fonction ou bien de sa définition.
I Eiffel étend ce mécanisme au cas des objets.
I Plusieurs difficultés apparaissent :
I Comment maintenir la cohérence globale d’un objet à travers les appels de différentes méthodes ?
I Comment sont véhiculées les spécifications à travers l’héritage ?

Une numérotation configurable de chaîne de caractères

I On se propose de définir un objet fournissant les services suivants :
I add (s) : associe un entier k à la chaîne s si ce n’est pas déjà fait. Dans le cas contraire, renvoie l’entier déjà associé à s.
I get (x) : renvoie la chaîne associée à l’entier x.
I upd (s, i) : associe l’entier i à la chaîne s si i n’est pas déjà utilisé.
I On suppose pour le moment que les chaînes de caractères sont initialisées.

Implantation en Eiffel

class NUM
creation {ANY}
make
feature {}
s_to_i : HASHED_DICTIONARY[INTEGER, STRING]
i_to_s : HASHED_DICTIONARY[STRING, INTEGER]
last_i : INTEGER
– Les propriétés à vérifier sur ces attributs :
valid_s_to_i_assoc (v : INTEGER ; k : STRING) : BOOLEAN is do
Result : = i_to_s.has (v) and then i_to_s.at (v) = k
end
valid_i_to_s_assoc (v : STRING ; k : INTEGER) : BOOLEAN is do
Result : = s_to_i.has (v) and then s_to_i.at (v) = k
end
dictionary_are_synchronized : BOOLEAN is
do
Result : =
s_to_i.for_all (agent valid_s_to_i_assoc)
and i_to_s.for_all (agent valid_i_to_s_assoc)
end
last_i_is_sup : BOOLEAN is
do
Result : = s_to_i.for_all (agent last_i ≥ ?)
end
Programmation Objet : Concepts Avancés
Implantation en Eiffel (suite)
feature {ANY}
make is
do
create s_to_i.make
create i_to_s.make
last_i : = 0
ensure
dictionary_are_synchronized
last_i_is_sup
end
unused (k : INTEGER) : BOOLEAN is
do
Result : = not (i_to_s.has (k))
end