L'objectif de ce bureau d'étude est de se familiariser avec la sémantique axiomatique en effectuant la preuve de quelques programmes Java.
Livraison
Livraison sur wdi.supelec.fr/Livraison avec le code H412
Les annotations sémantiques seront écrites en JML (Java Modeling Language), et traitées par l'outil Krakatoa dans Why.
- Saisir le programme
Produit.java
donné en exemple et le vérifier en tapant la commandekrakatoa Produit.java
dans un terminal. Le prouveur automatique Alt-Ergo doit permettre de valider toutes les obligations de preuve.
Note : lors du premier lancement de why, les prouveurs disponibles ne sont pas configurés, et vous aurez un message d'erreur. Il suffit d'exécuter la commandewhy3 config --detect-provers
, puis de relancer krakatoa. - Écrire en Java une classe Isqrt munie d'une méthode
static
calculant la partie entière de la racine carrée d'un entier en utilisant la propriété suivante : {$$n^2=\sum_{i=0}^{n-1}2i+1$$} Ajouter les prérequis, post-condition et invariant en JML pour démontrer que votre code calcule bien cette partie entière. Ajouter un variant pour montrer que le programme termine. Le code Java vous est fourni ci-dessous. - Faire de même avec un programme qui calcule le PGCD de deux entiers par soustractions successives. Il faudra définir un prédicat
gcd(integer x, integer y, integer d)
qui est vrai lorsque d est le PGCD de x et y. Vous aurez pour cela besoin d'un prédicatdivides(integer x, integer y)
qui indique si x divise y. - S'il vous reste du temps, utiliser Isabelle pour faire la preuve des lemmes introduits pour le pgcd (l'un d'eux n'est pas prouvé automatiquement), ou faire la preuve du tri par sélection.
Syntaxe JML
Les commentaires spéciaux contenant du JML sont de la forme : /*@ <code JML> @*/ ou //@ <code JML jusqu'en fin de ligne>
Vous ne pouvez mettre qu'un seul prédicat ou un seul lemme dans chaque commentaire spécial.
Les mots-clefs suivants peuvent être utilisés :
- requires
- pour donner une précondition :
requires n >=0 ;
- ensures
- pour donner une postcondition :
ensures \result == n*n ;
- loop_invariant
- pour donner l'invariant d'une boucle :
loop_invariant i+j == n ;
- loop_variant
- pour donner un variant d'une boucle (valeur qui décroit à chaque tour de boucle et reste positive ou nulle) :
loop_variant j - i;
- lemma
- pour donner un lemme (permet de guider le prouveur) :
lemma mul_distr_r: \forall integer a b c; (a+b)*c == a*c + b*c ;
- assert
- pour indiquer qu'une propriété est vraie à ce point du programme :
assert i > 0 && j > 0 ;
- predicate
- pour définir un prédicat logique :
predicate even(integer n) = n%2 == 0 ;
- \result
- pour faire référence à la valeur de retour d'une fonction
- \old
- pour faire référence à la valeur initiale d'une variable dans la postcondition :
\old(i)
- \at
- pour faire référence à la valeur précédente d'une variable un invariant :
\at(i,Pre)
- \forall
- pour le quantificateur universel :
\forall integer n; n+1 > n;
- \exists
- pour le quantificateur d'existence :
\exists integer k; 4 == 2*k ;
- ==>
- pour l'implication :
\forall integer x; x == 3 ==> x/2 == 1 ;
- <==>
- pour l'équivalence :
\forall integer x; x%2 == 0 <==> x == 2*(x/2) ;
- ghost
- pour introduire des variables fantômes qui instrumentent le code :
ghost integer gx = x ;
Exemple
Ce programme calcule le produit de deux entiers en n'utilisant que la somme, la différence et les décalages arithmétiques à gauche (multiplication par 2) et à droite (division par 2) :
La commande à utiliser pour vérifier ce code Java est : krakatoa Produit.java
Partie entière de la racine carrée d'un entier
Calcul du pgcd de deux entiers