Software Verification |
Si OCaml vous est un langage familier, vous pouvez passer à la suite. Sinon, ouvrez le document «Tuto-OCaml.pdf» (ou ici). Il vous présentera la plupart des concepts et syntaxes du langage dont nous aurons besoin durant le cours.
Z3 est un SMT-solveur de Microsoft Research. Il permet de décider la satisfiabilité de formules du premier ordre passées en paramètre. Ces formules peuvent parler de booléens, d’entiers, de réels, de tableaux, de fonctions abstraites, de bit-vectors, etc.
En cas de satisfiabilité, il permet de récupérer une affectation de variables satisfaisant la formule. En cas d’insatisfiabilité, il permet de récupérer une preuve d’indécidabilité.
Dans le cadre de ce TP, nous nous concentrerons sur la manipulation des entiers, et nous serons amenés à récupérer un modèle (cette partie vous sera donnée). Nous n’utiliserons pas l’intégralité de ses fonctionnalités. Nous l’utiliserons via son API OCaml, mais vous pouvez éventuellement jeter un œil au tutoriel suivant qui concerne Z3 lui-même, en regardant spécifiquement les sections «Basic Commands» (avant «Using Scopes»), Propositional Logic et Arithmetic.
Il est tout à fait facultatif de regarder en détail ce tutoriel, par la suite, on ne passera que par l’API Ocaml, l’exercice suivant est donc plus utile. Vous pouvez cependant le garder comme référence de ce qui est spécifique à Z3.
Nous nous tournons maintenant vers l’API de Z3 pour OCaml que nous utiliserons dans le reste du cours.
La documentation de l’API Z3 est accessible ici.
Keen est un jeu de logique que vous trouverez là. Il consiste à remplir une grille carrée de coté n avec des entiers de 1 à n tels que chaque entier n’apparaisse qu’une fois sur chaque ligne et sur chaque colonne. De plus, la grille est divisée en zones auxquelles sont associées une opération et un résultat : si l’opération est une addition (resp. multiplication), alors la somme (resp. produit) des nombre de la zone donne le résultat. Pour la soustraction et la division, les zones font nécessairement 2 cases et l’une des deux différences (resp. quotients) possibles doit être le résultat. Notez que dans le cas d’une division, le reste doit être nul.
Vous allez réaliser un solveur pour ce jeu. Tous les appels à Z3 et le parsing du jeu sont déjà implémentés, il ne vous reste plus qu’à créer la formule qui encode les contraintes du jeu. Chaque case sera représentée par une variable entière (qui représente le contenu de la case). Les questions 2 à 5 de cet exercice sont là pour vous guidez dans la conception de votre réduction (car c’en est une).
This document was translated from LATEX by HEVEA.