Formation informatique d Eiffel en pdf


Télécharger Formation informatique d Eiffel en pdf

★★★★★★★★★★3.5 étoiles sur 5 basé sur 1 votes.
Votez ce document:

Télécharger aussi :


Programmation Objet : Concepts Avancés

Cours 8 : Contrat, Test et Preuve

Yann Régis-Gianas

PPS - Université Denis Diderot – Paris 7

12 décembre 2008

Programmation par « contrat »

Le mal de l’ingénierie du logiciel

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 »?

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))

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.

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.


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


Invariants des objets

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)

Héritage des spécifications

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.

Analogie entre typage et spécification

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.

Retour sur notre exemple

class NUMBIS

inherit

NUM redefine make, add, upd, get end

creation

make feature {ANY}

make is

do

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

else

Result : = Precursor (s) end

ensure then

s = Void implies Result = 0 end

get (x : INTEGER) : STRING is require else x = 0

do if x = 0 then

Result : = Void

else

Result : = Precursor (x) end

ensure then

x = 0 implies Result = Void end

upd (x : INTEGER; s : STRING) is require else

unused (x) s = Void implies x = 0

do

if s /= Void then

Precursor (x, s) end end


Vérification partielle des contrats

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 !

Vérification totale des contrats

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.

Preuve formelle sur machine

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

Preuve formelle de programmes sur machine

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

Vérification statique d’une classe Java

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]

Des problèmes encore ouverts

I Ces systèmes ont des difficultés à traiter le partage de références entre objets.

I Il est aussi très difficile 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.



168