L'objectif de ce bureau d'étude est de se familiariser avec la sémantique axiomatique en effectuant la preuve de quelques programmes Java.

Les annotations sémantiques seront écrites en JML (Java Modeling Language), et traitées par l'outil Krakatoa dans Why.

1. Écrire en Java une class 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}^{k-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.
2. Faire de même avec un programme qui calcule le PGCD de deux entiers par soustractions successives.
3. S'il vous reste du temps, faire de même avec le 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>

Les mots-clefs suivants peuvent être utilisés :

requires

pour donner une précondition

ensures

pour donner une postcondition

loop_invariant

pour donner l'invariant d'une boucle

loop_variant

pour donner un variant d'une boucle (valeur qui décroit à chaque tour de boucle et reste positive ou nulle)

lemma

pour donner un lemme (permet de guider le prouveur)

assert

pour indiquer qu'une propriété est vrai à ce point du programme

predicate

pour définir un prédicat logique

\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

\forall

pour le quantificateur universel

\exists

pour le quantificateur d'existence

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 : gwhy Produit.java