Vous êtes ici : FIL > Portail > Master Informatique > M1S2 > SVL

Spécification et Validation du Logiciel - SVL

Cette option se déroule au S6 du Master 1 informatique.

Intervenants

Mirabelle Nebut

Volume horaire

L'unité comporte une séance de cours-TD hebdomadaire de 1h30 et une séance de TD-machine hebdomadaire de 2h.

Pré-requis

Pour apprécier cette UE, un attrait pour la conception OO du logiciel et pour les aspects formels de l'informatique est souhaitée. Si le pattern d'injection des dépendances (pour le test) ou les formules logiques (pour les méthodes formelles) vous donnent de l'urticaire, il vaut mieux choisir une autre option (même si vous pensez faire plus tard un master IAGL).

Compétences requises:

  • pour la partie test : la programmation et des notions de conception objet (la connaissance de Python n'est pas requise).
  • pour la partie approches formelles : les bases de la théorie des ensembles et de la logique du premier ordre.

Crédits

5 ECTS
Mirabelle Nebut
dernière modification : 26/11/2016 à 17:05:03

Objectifs

L'UE vise à sensibiliser les étudiants aux méthodes permettant de développer des programmes fiables et de qualité. L'UE se décompose en 2 parties de 6 semaines, au contenu volontairement très différent:
  • test unitaire du logiciel;
  • approche formelle pour la vérification de modèles du logiciel.
On commencera d'abord par le test (plus intuitif et proche de ce que les étudiants connaissent) avant de passer au formel (nettement plus dépaysant):
  • le test du logiciel, indispensable en entreprise, fait partie de la sphère quotidienne du développeur : pas de logiciel de qualité sans suites de test qui passent ! La pratique du test est une école de la rigueur, qui oblige à repenser les processus de développement, et produit des applications testables donc mieux conçues, et testées donc plus fiables;
  • les méthodes formelles de validation du logiciel sont beaucoup moins utilisées au quotidien que le test. Certaines (comme le model-checking) sont le plus souvent réservées aux applications critiques ou spécifiques, comme les protocoles de communication. D'autres s'appliquent à la conception et au développement du logiciel mais effraient les concepteurs et les développeurs à cause du formalisme qui nécessite un apprentissage. En tout état de cause il est utile d'en avoir entendu parler pour savoir quoi en attendre.

Contenu

Test

Le contenu de cette partie sera modulé en fonction des compétences préalables des étudiants participant au module.

L'UE présente différents aspects du test de programmes : place et importance du test dans le développement logiciel, automatisation des tests, stratégies de test unitaire, notion de couverture de test, test d'acceptation. On insiste sur les méthodes de développement "pensez au test en premier" en pratiquant le Test Driven Development.

On utilisera le langage Python mais les principes (méthodes, outillage) présentés dans l'UE valent pour n'importe quel langage de programmation objet. La connaissance de Python n'est pas un pré-requis (il suffit de maîtriser un langage objet), par contre un attrait pour la conception 00 du logiciel est souhaitable. Le travail personnel portera principalement sur la pratique : en plus des TPs d'apprentissage, les étudiants seront fortement incités à réutiliser leurs compétences dans les autres UEs et projets du semestre.

À l'issue de l'UE, les étudiants doivent:

  • être conscients de la nécessité de tester le code qu'ils écrivent, quel que soit son contexte;
  • pouvoir discuter des intérêts de l'approche dirigée par les tests (TDD), savoir spécifier un programme par ses tests;
  • connaître les concepts du test unitaire/d'interaction, être capables d'utiliser une bibliothèque dédiée pour un langage objet;
  • connaître quelques critères de couverture de code, être conscients de leurs limites, être capables d'utiliser une bibliothèque de calcul de couverture;
  • savoir appliquer la notion de test aux limites;
  • connaître les principes du test d'acceptation, savoir utiliser un outil de test d'acceptation pour application web;
  • être conscients des limites intrinsèques du test.

On utilisera tout ou partie des outils suivants: unittest et nose pour les tests unitaires, sphinx et doctest pour la documentation, mockito pour les tests d'interaction, coverage pour la couverture de code, selenium et cherrypy pour le test d'acceptation, cucumber pour le "développement dirigé par les comportements" (behavioral-driven development ou BDD), Hypothesis pour le property-based testing.

Approches formelles

Le but de cette partie plus théorique est de faire découvrir aux étudiants le monde des spécifications et des approches formelles. L'UE ne se spécialisera pas sur une méthode en particulier (changement par rapport aux années passées), mais présentera plusieurs approches, sans prétendre à l'exhaustivité, et en restant proche du développement et de la conception logiciels. L'idée est que les étudiants sachent ce qu'on peut attendre d'une méthode formelle (quelles propriétés d'un programme peut-on prouver ?), et aient une idée de l'effort à fournir pour y parvenir.

L'UE abordera essentiellement la spécification à base de contrats (on fera un petit détour par la programmation par contrat). On verra ensuite comment on peut vérifier qu'un programme est conforme à ses contrats (et si c'est toujours possible). On utilisera notamment des méthodes d'exécution symbolique et des solveurs pour la satisfaisabilité modulo théorie (SMT). On fera le lien avec la partie test en abordant par ex leur génération automatique. Suivant l'avancement du cours on pourra regarder le model-checking avec Spin, la preuve de programme en C# avec Spec# (RiSE), l'interprétation abstraite avec Contracts (RiSE), le model-checking borné avec Alloy.

Le pré-requis est d'avoir un attrait pour les aspects formels de l'informatique, et d'avoir des connaissances de base en automates, logique du premier ordre, théorie des ensembles.

À l'issue de l'UE, les étudiants doivent:

  • savoir énumérer quelques types de méthodes formelles existants, être conscients de leurs avantages et inconvénients (notamment par rapport au test);
  • avoir intégré la nécessité d'une abstraction des programmes, la plupart des méthodes formelles s'appliquant à un modèle du programme et non à son implémentation, trop bas niveau et détaillée;
  • connaître les concepts de la spécification par contrats;
  • avoir compris les notions de logique décidable/indécidable, de complétude et de sûreté d'une analyse.

Mirabelle Nebut
dernière modification : 26/11/2016 à 17:02:58
Horaires des cours de SVL pour 2017-2018 :
  • CTD: jeudi 8h15-9h45 en A1 - M5
  • TP: jeudi 10h-12h en A15 - M5
Mirabelle Nebut
dernière modification : 09/01/2018 à 09:44:43
Séance Cours-TD TP Remarque
1 du 15/01 au 20/01 intro au test / rappels, rudiments de test fonctionnel,
demo unittest, doctest
tp1, découvrir l'envt de travail python
2 du 22/01 au 27/01
3 du 29/01 au 03/02
4 du 05/02 au 10/02
5 du 12/02 au 17/02
6 du 19/02 au 24/02
du 26/02 au 31/03 interruption pédagogique hiver
7 du 05/03 au 10/03
8 du 12/03 au 17/03
9 du 19/03 au 24/03
10 du 26/03 au 31/03
11 du 02/04 au 07/04
12 du 9/04 au 14/04
13 du 16/04 au 21/04
du 23/04 au 05/04 interruption pédagogique de printemps
13 du 07/05 au 12/05
Mirabelle Nebut
dernière modification : 12/01/2018 à 15:40:12

L'évaluation est basée sur un contrôle continu englobant les TPs réalisés et deux interrogations écrites.

Deux interrogations écrites auront lieu:

  • interrogation écrite sur le test à la fin de la partie test, note Itest
  • interrogation sur les approches formelles pendant la prmeière session des examens du M1 S2, note Iformel
Ces interrogations écrites ne seront pas rattrapées (même en cas d'absence ou de note inférieure à la moyenne) avant l'examen de seconde session qui regroupera les parties test et approches formelles.

La note de TP TP, sur 20, inclut les TPs évalués et éventuellement d'autres travaux de type exposé. Les TPs sont rendus sur PROF ou Moodle à la fin de chaque séance de TP, par binôme, et permettent un retour pédagogique régulier. Un TP non rendu sur PROF ou Moodle est un TP non rendu (il est conseillé de faire des dépôts sur PROF au long de la séance). Un étudiant absent lors de la séance doit en avertir l'enseignant, suite à quoi son évaluation sera éventuellement adaptée pour ce TP.

La note finale sur 20 (N) est calculée comme une moyenne pondérée de ces trois notes :

N = SUP(I, (TP + 2*I)/3) avec I = (Itest + Iformel)/2

Lors de la seconde session d'examen la note TP est conservée, la note d'interrogation écrite (I = (Itest + Iformel)/2) est remplacée par la note I2 obtenue lors de la seconde session, le calcul se faisant par:

N = SUP(I2, (TP + 2*I2)/3)

L'unité acquise apporte 5 ECTS.

M. Nebut

Exposés:

Sujet de projet

Cours-TD Test

CTD1 Rappels sur le test, test unitaire et documentation avec Python3

  • transparents d'intro au test
  • démo unittest: mot_max.py et test_mot_max.py
  • rudiments de test fonctionnel, fiche
  • exercice: écriture de tests unitaires et doctest
  • les notes de Martin Monperrus (Level 1 pour ce CTD)
  • Pour ceux qui n'ont jamais fait de test, résumé issu du cours de COO en L3 incluant JUnit et la méthodo TDD.

CTD2 Test en isolation, test des interactions, Mockito pour Java

  • lecture obligatoire : fiche synthétique sur le test des interactions
  • lecture obligatoire : fiche synthétique qui résume Mockito
  • fiche exercices

CTD3 TDD sans dépendances

  • lecture obligatoire : fiche synthétique sur le TDD
  • Retour sur l'exercice MyJunit (test des interactions)
  • Démo à partir de l'exemple du TP1

CTD4 TDD avec les dépendances, mocks

CTD5 TDD et COO, architectures testables

CTD6, suite du CTD5.

CTD7, property-based testing.

Cours-TD Approches formelles

TP

Les TPs se font obligatoirement en binôme selon le principe de la programmation en binôme (l'un a le clavier et propose, l'autre commente), en alternant le clavier par tranches de 25 minutes. On travaillera par tranches de 25 minutes suivies de 5 minutes de pause, sans oublier le rendu sur PROF.

L'archive rendue sur PROF doit être intitulée

TPX_loginetudiant1_loginetudiant2.tgz (ou zip)

sans espaces, en reprenant le login université (de la forme prenom.nom). De même les noms de fichiers ou de répertoire ne doivent pas contenir d'espaces. L'archive contiendra systématiquement un README indiquant le travail réalisé et les éventuelles difficultés rencontrées (notamment si un test ne passe pas !)

TP1: sur unittest et doctest sujet, source tp1.py

TP2 test des interactions avec Mockito pour Java sujet. Mockito n'est pas installé au M5. Son jar et ses dépendances sont dans /home/enseign/SVL/Mockito/. Vous pouvez tenter Eclipse : dans les propriétés du projet, onglet Libraries, bouton add external jar, et ne pas oublier de créer des cas de tests pour JUnit4 et pas JUnit Jupiter. Vous pouvez utiliser la ligne de commande en ajoutant les .jar au CLASSPATH, sans oublier Junit4 et ses dépendances qui sont dans /usr/share/java/ (par ex junit4.jar et hamcrest-all.jar). Par ex :

export CLASSPATH=/home/SVL/Mockito/byte-buddy-1.7.9.jar:/home/SVL/Mockito/mockito-core-2.13.3.jar:
  /home/SVL/Mockito/objenesis-2.6.jar:/usr/share/java/junit4.jar:/usr/share/java/hamcrest-all.jar:classes:$CLASSPATH   
javac -d classes -sourcepath src test/casino/TestJouerAuCasino.java
java  org.junit.runner.JUnitCore casino.TestJouerAuCasino

TP3: TDD sans dépendances avec JUnit sujet

TP4: TDD avec dépendances sujet

TP5 : tester avec des ES

TP6 : révision des SOLID en test sujet login.

TP7 : property-based testing avc Hypothesis

  • Commencer par installer Pytest et Hypothesis dans votre envt virtuel pour SVL
  • expérimenter avec Hypothesis sur la démo et l'exercice "sous-echantillonnage"
  • exploration de la stratégie floats() (génération de réels) :
    • écrire un test Hypothesis qui teste que, pour tout x réel, x vaut - (- x). Comprenez-vous le retour d'Hypothesis ? Regardez la doc de floats pour supprimer l'erreur.
    • écrire un test Hypothesis qui teste que, pour tout réel x, x + 1 est strictement plus grand que x. Comprenez-vous le retour d'Hypothesis ? Quel type d'erreurs liées à l'utilisation de flottants le property-based testing permet-il de détecter ?
  • Reproducibilité des tests : généralement on lance les tests plusieurs fois de suite. Pensez-vous possible qu'un test écrit en PBT passe lors d'un premier lancer puis ne passe pas lors d'un second lancer ? Inversement, pensez-vous possible qu'un test écrit en PBT échoue lors d'un premier lancer puis passe lors d'un second lancer ? Quel cas n'est pas souhaitable / pas grave ? Argumenter.

Documentation

Python

Nous utiliserons Python3 en SVL:

  • au M5 la version par défaut de Python est la 2.7
  • la version 3.5.2 est accessible par python3
  • si vous rencontrez des problèmes d'encodage, vous êtes peut-être en python2. Pour connaître les différences entre les 2 versions (non compatibles)

Quand on vient du monde Java :

  • le self est obligatoire
  • on ne peut pas utiliser le même nom pour un attribut et une méthode
  • pas de déclarations

Le module unittest alias pyunit

  • vient avec Python
  • la doc
  • dans la doc, les assertions
  • ou help(unittest), help(unittest.TestCase), etc
  • NB sur le assertEqual : contrairement au assertEqualS de JUnit, pas d'ordre imposé sur les paramètres (expected, actual). On choisit un ordre et on s'y tient.
  • unittest ne propose pas de tests paramétrés, voir nose2

Environnement virtuel pour Python

  • Permet d'installer facilement les outils Python pour SVL
  • La doc du M5 est pour virtualenv.
  • Ou utiliser venv. Créer dans votre répertoire dédié à SVL (ou ailleurs) un répertoire pour l'installation.
  • Dans ce répertoire, copier le fichier install_env_svl.sh
  • exécuter le script par sh install_env_svl.sh : c'est à faire une fois, et à refaire à chaque fois que l'installation change.
  • Quand on veut utiliser les outils installés dans un terminal, faire un source .../bin/activate où ... est le répertoire qui contient env_svl. Observer le changement de l'invite. Les exécutables Python sur lesquels pointe votre PATH sont maintenant ceux de env_svl.
  • Pour revenir à l'environnement initial, taper deactivate.

Nose2

  • le site officiel. Remplace nose
  • nose2 collecte puis exécute tous les fichiers, classes et fonctions/méthodes, répertoires incluant le mot test ou Test.
  • On peut aussi lancer un fichier de test seulement par nose2 test_bidon.py (mais pas adapté pour exécuter la doctest ?)
  • les options de nose2 :
    • -v pour afficher le détail des tests qui sont exécutés (affiche la docstring du cas de test si elle existe à la place de son nom).
    • --plugin nose2.plugins.doctests --with-doctest pour tester la documentation (modules, classes, fonctions, méthodes).

Le module doctest

  • la doc : permet d'écrire des "tests de la doc", soit des docs exécutables décrivant les usages pur votre code applicatif. À écrire dans les docstring de votre code applicatif, pas dans les tests !
  • exécution avec nose2 : nose2 -v --plugin nose2.plugins.doctests --with-doctest
  • sans utilisation de l'option -v l'exécution de la doctest ne produit aucune sortie si pas d'erreur
  • avec nose2 : pas adapté pour lancer la doctest d'un fichier en particulier, utiliser directement python3 (cf plus bas)
  • pour les exceptions : doctest ne prend en compte que la ligne Traceback etc puis la ligne contenant le nom de l'exception et les suivantes. On pourra donc supprimer les autres et utiliser une ellipse (même si l'ellispe n'est pas prise en tant que telle ici):
    >>> s.ajouter_reference("ref1")
    Traceback (most recent call last):
    ...
    ValueError																		    
  • exécution avec python : terminer le module toto par
    								  
    if __name__ == "__main__":
        import doctest
        doctest.testmod()								  
    
    et lancer python3 -v toto.py
  • autre exécution avec python (shortcut pour testmod qui ne marche pas toujours) : python3 -m doctest -v toto.py

JUnit

TDD et méthodes agiles (pro-TDD)

TDD et unit testing: les contres et les nuancés

Dans la série "TDD is dead": Dans la série "Why Most Unit Testing is Waste", chez RBCS:

TDD et mocks : Mocks Aren't Stubs

Module python mockito

  • Le site officiel et une petite doc
  • fiche qui résume mockito
  • installé au M5 pour python3
  • pour ceux qui ont des soucis d'installation sur leur machine perso, avec un message ressemblant à ça :
    ...
        Traceback (most recent call last):
          File "./distribute_setup.py", line 143, in use_setuptools
            raise ImportError
        ImportError
    ... could not build the egg.
    
    vous pouvez essayer d'installer cette autre version, par ex avec pip3 install --user mockito-without-hardcoded-distribute-version-0.5.4.tar.gz

Couverture de code avec Nose et coverage

  • Le site officiel du module coverage
  • coverage est installé au M5
  • si sur votre machine perso nose ne voit pas coverage, essayer d'ajouter le répertoire contenant coverage dans le PATH

Pour lancer coverage via nose :
  • nosetests --cover-html --with-coverage --cover-erase --cover-branches --cover-package=bidon test_bidon.py
  • --with-coverage --cover-erase pour lancer coverage sans repartir des résultats précédents, affichage d'un rapport textuel de la forme:

    Name                    Stmts   Miss  Cover   Missing
    -----------------------------------------------------
    restaurant_entreprise      55      4    93%   120, 220-222
    ----------------------------------------------------------------------
    Ran 18 tests in 0.057s
    
  • --cover-package=nom_package pour lancer coverage sur ce module uniquement
  • --cover-branches pour demander la couverture des branches
  • --cover-html pour demander la génération d'un rapport au format html (dans un répertoire cover par défaut, peut-être modifié)

Si la version pour python3 de coverage n'est pas installée, alors l'installer en local:

pip3 install --user nose coverage
crée un répertoire .local à la racine de votre compte s'il n'existe pas déjà. Ensuite utiliser cette version dans votre terminal après avoir entré:
export PATH=$HOME/.local/bin:$PATH
Si ça ne marche pas, essayer avec ça:
export HTTP_PROXY=http://cache-etu.univ-lille1.fr:3128

Selenium

  • le site officiel
  • une readthedocs sur Selenium WebDriver
  • la doc de Selenium IDE
  • pour installer Selenium IDE sur Firefox, depuis la page download, chercher "selenium IDE" pour l'installer depuis addons.mozilla.org
  • pour installer selenium webdriver sur votre machine perso: pip3 install --user --upgrade selenium, installer aussi le driver geckodriver et l'ajouter dans le PATH
  • le driver pour Chrome est à télécharger, l'exécutable chromedriver devant se trouver dans le PATH

Bottle

  • le site officiel
  • install sur votre machine perso: pip3 install --user --upgrade bottle

Behavior Driven Development

  • L'histoire (fictive) d'une équipe qui se met au test d'acceptation / au BDD / à la spécification par l'exemple, écrite par Alistair Scott.
  • une présentation sur le site de Behave (attention les oracles de la classe TestList sont de pures horreurs), inspirée de la page wikipedia ci-dessous
  • sur wikipedia, le BDD comme approche comportementale du test d'acceptation impliquant toutes les parties prenantes d'un projet, y compris (et surtout) les non-informaticiens
  • approches connexes: Acceptance test-driven development, Specification by example
  • BDD et TDD sur le BDDwiki, à lire au moins pour la description faite du TDD
  • une intro détaillée par Dan North, expliquant l'historique du pourquoi du comment et donnant un éclairage intéressant sur le TDD
  • le BDD, certains l'aiment et d'autres non

Outillage pour le BDD

  • Cucumber, l'outil de référence
  • Behave, un portage de Cucumber pour Python
  • sur le site de Behave, une comparaison avec les outils existants
  • pour lancer Behave en ne lançant pas les scenarios "tagués" par todo : behave --tags=-todo

JML : programmation par contrats pour Java

  • JML homepage
  • openJML, une des distributions (qui supporte Java7), et ici
  • openJML sur rise4fun
  • le manuel de référence de JML
  • pour compiler des programmes Java avec openJML:
    java -jar $OPENJML/openjml.jar -rac -racCompileToJavaAssert -d classes src/mon_package/*.java
    
  • pour exécuter des classes Java compilées avec openJML:
    java -ea -cp classes:$OPENJML/openjml.jar:.:$CLASSPATH mon_package.MaClasse

Spec# : contrats en C# et vérification avec Boogie

Contracts: contrats et interprétation abstraite

Microsoft Research in Software Engineering (RiSE)

Logique de Hoare, transformateurs de prédicats de Dijkstra

  • un résumé de la logique de Hoare, sur la page de Fabrice Rossi
  • Hoare et Dijkstra, Forward with Hoare, chapitre de livre écrit pour l'occasion des 40 ans de la logique de Hoare

Hypothesis, property-based testing pour Python

Property-based testing

PyExZ3, exploration de programmes Python par exécution symbolique dynamique

  • pas installé au M5
  • le site sur github, download et doc succinte
  • utilise le prouveur Z3 (installé au M5) pour calculer la satisfaisabilité des expressions logiques
  • l'exécutable z3 doit être dans le PATH et le PYTHONPATH
  • ne marche que pour du Python fonctionnel pur (pas pour Python objet)
  • l'exploration s'arrête si exécution d'une assertion ou levée d'exception
  • un papier qui décrit formellement l'outil
  • python3 pyexz3.py --start=ma_fonction mon_module.py

Z3, un solveur SMT (satisfaisabilité modulo théorie)

  • site officiel
  • RISE4fun pour essayer Z3 en ligne sur Rise for fun, avec tutoriel
  • API pour Python: le module z3

Pex : concolic testing et contrats

  • le site
  • pex for fun, pour essayer en ligne, les bases de Pex for fun (on tombe soit sur une exécution de Pex classique, soit sur un coding duel - trouver grâce à Pex une implem secrète)
  • pex for fun avec code contracts, le mode "contracts" s'active aussi automatiquement avec using System.Diagnostics.Contracts;
  • Pex est devenu IntelliTest, disponible sous Visual Studio depuis 2015, en passant par SmartTest. Voir ici et pour comprendre comment sont générés les tests, et le manuel de référence.

Vérification, divers

  • More than one way (also in verification), un article du blog bugcounting, qui montre sur un ex comment des outils de vérification appartenant à la même mouvance ont leurs particularités et obtiennent des résultats différents.
  • Dimensions in program verification, un article du blog bugcounting, qui classe différentes méthodes selon les 3 axes : correction (soundness, correctness = si l'outil dit que le programme est correct, c'est qu'il l'est vraiment), largeur du spectre des programmes et spécifications couverts (flexibility) et degré d'automatisation
  • théorème de Rice et impact pratique sur wikipedia

Méthodes (très) formelles et success stories

Programmation par contrats

Module contract pour Python

  • description synthétique
  • téléchargement de l'archive
  • le PYTHONPATH doit contenir le chemin d'accès au répertoire qui contient contract.py
  • attention ce module n'est utilisable en l'état que pour python2
  • attention le implies n'est pas paresseux, implies(b, alors, sinon) évalue alors même si b vaut faux.
  • attention ne pas appeler dans un invariant de classe un accesseur de la même classe (sinon la bibliothèque évalue l'invariant en fin d'appel et récursion infinie)

Mockito pour Java

  • le site officiel de mockito
  • l'API de la version courante (lien "documentation" sur le site officiel)
  • le "tutoriel mockito" est la javadoc de la classe Mockito
  • fiche qui résume Mockito

Test et/ou OO en général :

  • la librairie de contraintes hamcrest
  • le site de xUnit patterns
  • Perfecting OO s Small Classes and Short Methods un article sur le sujet
  • un article sur les 10 points qui rendent votre code non testable. Attention, les points 7 et 8 rendent le code testable, les autres points le rendent non testable.
  • un message de blog expliquant comment mal utiliser une bibliothèque de mocks puissante peut renforcer ue mauvaise conception.
  • tenté d'implanter maintenant une fonctionnalité qui ne sera mise en production que plus tard ? le principe de YAGNI expliqué par Martin Fowler.
  • levée d'exception ou non ? Le cas de la validation des données par Martin Fowler
  • More Typing, Less Testing: TDD with Static Types, par Ken Fox, part1 et part2

Concernant Spin :

Autres cours de test

Annales

Les sujets ci-dessous sont partiellement périmés au sens où le contenu du cours change chaque année.

Mirabelle Nebut
dernière modification : 15/03/2018 à 11:21:09