Vérificateur d’assertions à runtime : un exemple simple avec OCaml

Dans le cadre de ma formation, Pierre et moi avons eu à réaliser un vérificateur d’assertion à runtime. J’avais déjà parlé du JML en donnant les ressources montrant que le JML était un langage d’assertions à runtime, et donc permettait de rajouter des spécifications formelles à son code. Le but étant de rajouter encore de la sémantique au code, et de permettre au programme de s’arrêter (de préférence, proprement), s’il se rend compte que la liste d’instruction qu’il va (ou qu’il vient d’)exécuter n’est pas conforme à ce qui était prévu.

Bref : prenons un exemple. Pour un langage, disons qui ressemblerait au C (pour que tout le monde comprenne), voilà une fonction que l’on pourrait avoir :

float diviser (int personnes, int bonbons){
float result = bonbons / personnes;
return result;
}

Or, cette fonction peut planter méchamment s’il s’avère qu’elle est amenée à être appelée lorsque personnes = 0.

Donc on s’arrange pour rajouter de la sémantique fonctionnelle comme suit :

//@@ requires (personnes != 0)
float diviser (int personnes, int bonbons){
float result = bonbons / personnes;
return result;
}

Ce qui, une fois compilé (en fonction du compilateur, bien sûr), pourra donner un code machine ressemblant à celui qu’auraient données ces lignes de code :

float diviser (int personnes, int bonbons){
float result;
if (personne != 0) { result = bonbons / personnes; }
else { raise (« Error condition »); }
return result;
}

Donc comme vous pouvez le voir, les spécifications sémantiques ont été traduites en conditions dans le code.

Bref : j’ai eu à faire avec Pierre un vérificateur d’assertion à runtime (vérificateur d’assertion à runtime = compilateur mettant les spécifications dans le code). Ce compilateur a été fait en OCaml, en définissant un langage d’exemple simplifié appelé PL, et son langage d’assertions PLML.

Pour revenir à ce que je disais tout à l’heure, dans l’exemple ci-dessous (en langage PL/PLML), on peut voir les IfThenElse qui ont été rajouté dans le code entre l1 et l2 :

Voici ci-dessous le rapport, qui vous expliquera progressivement ce que nous avons fait. Je vous en conseille la lecture, si les spécifications formelles vous intéressent, c’est un domaine de l’informatique (à mon avis) assez méconnu, et pourtant, il y a de jolies choses à y voir.

Le code du projet peut être téléchargé là, et vous pouvez télécharger l’interpréteur OCaml sur la page du projet.

Si vous avez des questions à poser, orientez-vous plutôt vers Pierre si c’est pour le PL (interpréteur et tout), et plutôt vers moi pour ce qui est du PLML.

Laisser un commentaire

Votre adresse e-mail ne sera pas publiée. Les champs obligatoires sont indiqués avec *

Ce site utilise Akismet pour réduire les indésirables. En savoir plus sur comment les données de vos commentaires sont utilisées.