Si le téléchargement ne démarre pas apràs 5 secondes, veuillez cliquer sur le lien "Télécharger"
Cours 8 : Contrat, Test et Preuve
Yann Régis-Gianas
PPS - Université Denis Diderot – Paris 7
12 décembre 2008
Deux « hypocrisies » de l’industrie du logiciel (E.W. Dijkstra)
I La maintenance informatique : un logiciel peut-il s’user?
I Les fameux bugs : pourquoi ne pas les appeler « erreurs »?
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 » ...
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))
IP est la précondition, spécifiant le domaine correct d’utilisation.
IQ est la postcondition, spécifiant la relation logique liant l’entrée et la sortie.
#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))); }
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.
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.
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!
1. Le langage Eiffel qui est centré sur la programmation par contrat.
2. Les outils de vérification statique pour les langages à objet.
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.
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
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?
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.
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 : = (v) and then (v) = k end
valid_i_to_s_assoc (v : STRING; k : INTEGER) : BOOLEAN is do
Result : = (v) and then (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
feature {ANY}
make is
do
create create
last_i : = 0
ensure
dictionary_are_synchronized last_i_is_sup
end
unused (k : INTEGER) : BOOLEAN is do
Result : = not ( (k)) end
add (s : STRING) : INTEGER is require
s /= Void
dictionary_are_synchronized last_i_is_sup
do
if (s) then
Result : = (s)
else
last_i : = last_i + 1 (last_i, s) (s, last_i)
Result : = last_i end
ensure
dictionary_are_synchronized last_i_is_sup old Current.unused (Result) get (x) = s end
get (x : INTEGER) : STRING is require
(x) dictionary_are_synchronized last_i_is_sup
do
Result : = (x) ensure
dictionary_are_synchronized
last_i_is_sup
add (s) = x end
upd (x : INTEGER; s : STRING) is require
s /= Void
dictionary_are_synchronized last_i_is_sup unused (x)
do
(x, s) (s, x)
ensure
dictionary_are_synchronized
last_i_is_sup get (x) = s
add (s) = x
end end
I On remarque que les propriétés dictionary_are_synchronized et last_i_is_sup doivent être valides avant et après chaque appel de méthode.
I Cette propriété est un invariant de notre objet.
I Elle peut être invalidée au cours de l’exécution d’une méthode.
I Eiffel fournit un mécanisme pour déclarer les invariants d’un objet. I Dans notre exemple, on rajoute :
invariant dictionary_are_synchronized last_i_is_sup à la fin de la définition de la classe.
Un bug, pardon, « une erreur » dans notre exemple !
(en fait, il y en a même deux)
I On déclare une classe fille qui redéfinit la méthode add. La nouvelle version de cette méthode accepte les chaînes non initialisées et leur associe systématiquement l’entier 0.
I Pour les mêmes raisons qui imposent une contra-variance des arguments des méthodes dans les sous-classes, la précondition de redéfinition d’un méthode doit être plus faible que la précondition initiale.
I En d’autres termes, les préconditions des méthodes de la classe fille doivent impliquer logiquement les préconditions des méthodes de la classe mère.
class NUMBIS
inherit
NUM redefine make, add, upd, get end
make feature {ANY}
make is
Precursor
– 0 is reserved for Void last_i : = 1 end
add (s : STRING) : INTEGER is require else
True do
if s = Void then
Result : = 0
Result : = Precursor (s) end
s = Void implies Result = 0 end
get (x : INTEGER) : STRING is require else x = 0
do if x = 0 then
Result : = Void
Result : = Precursor (x) end
x = 0 implies Result = Void end
upd (x : INTEGER; s : STRING) is require else
unused (x) s = Void implies x = 0
if s /= Void then
Precursor (x, s) end end
I Une fois le développement du programme et de sa spécification achevé, on peut tester la conformité du programme à sa spécification à l’aide :
I de tests unitaires : on isole un objet et on vérifie que les invariants et les postconditions sont valides pour des entrées conformes aux préconditions.
I de tests d’intégration : on isole des groupes d’objets et on vérifie que les préconditions des méthodes sont validées.
I Il existe des outils pour gérer et automatiser les jeux de tests (JUnit, Quickcheck, ...) I mais ...
Un test n’est pas une preuve !
I Des outils modernes (majoritairement issus de la recherche) s’attaquent à la preuve formelle de la correction des programmes vis-à-vis de leur spécification.
I Tous s’appuient sur une formalisation mathématique de la sémantique des langages de programmation et sur une mécanisation du raisonnement logique.
Un ordinateur peut manipuler des preuves.
I Certains formalismes permettent d’exprimer les propriétés des programmes. I Des outils les implémentent et permettent de vérifier des preuves sur ordinateur (Coq, PVS, Isabelle/HOL, ...).
I D’autres outils permettent même d’effectuer des recherches automatiques de preuve (en général dans des logiques moins riches, comme la logique du premier ordre).
I La phase 1 est du ressort du programmeur.
I La phase 2 est un algorithme automatique.
I La phase 3 peut être traitée par :
I Des prouveurs automatiques pour les preuves « faciles » ;
I Le programmeur dans un assistant de preuve pour les démonstrations « subtiles ».
I L’outil Krakatoa, intégré à la plateforme Why, est développé au LRI de l’Université Paris 11.
I Il permet de prouver de nombreuses propriétés des programmes Java en utilisant la méthode de Hoare. I D’autres outils sont actuellement développés un peu partout dans le monde :
ESC/Java, SPEC#, FOCAL, ...
I [Démonstration]
I Ces systèmes ont des difficultés à traiter le partage de références entre objets.
I Il est aussi très d
ifficile de savoir comment réutiliser les preuves à travers l’héritage.
I La notion d’invariant de classe semble aujourd’hui trop rigide pour spécifier des programmes réalistes : il arrive qu’un objet brise l’invariant d’autres objets temporairement, sans mettre en cause la correction d’un programme.
