Attrapez un chat avec TLA +

Les méthodes formelles sont considérées comme un moyen efficace mais déraisonnablement complexe d'assurer la fiabilité des logiciels. Les outils utilisés pour cela diffèrent considérablement de ceux familiers au programmeur. Cet article est écrit dans le but d'abaisser le seuil d'accès à cette boîte à outils. J'utiliserai le système de vérification des modèles non pas pour résoudre des tâches de formulation de logiciels difficiles à formuler, mais pour résoudre un casse-tête compréhensible même pour les écoliers.

Vous êtes dans un couloir direct avec sept chambres d'un côté. Dans l'un d'eux est un chat. En une seule étape, vous pouvez regarder dans l'une des pièces, s'il y a un chat, il est pris. Dès que la porte se ferme, le chat emménagera dans l'une des pièces voisines de celle dans laquelle il se trouvait. La tâche consiste à attraper le chat.

TLA + et logique temporelle

Il existe de nombreux outils qui peuvent résoudre de tels problèmes. Souvent, dans de tels cas, des solveurs SMT sont utilisés. En règle générale, ces systèmes utilisent la logique de prédicat habituelle et exprimer la séquence d'actions est assez compliqué (vous devez utiliser quelque chose comme un tableau, ce qui n'est pas très pratique pour travailler avec). TLA + utilise une logique temporelle, qui permet d'utiliser l'état d'un système dans une instruction à la fois à l'étape actuelle et à l'étape suivante.

CatDistr' = CatDistr \ {n} 

Cette condition stipule que l'ensemble des pièces dans lesquelles le chat peut se trouver après avoir vérifié la pièce n coïncide avec l'ensemble des pièces d'où n a été prélevé (si le chat était là, il est attrapé et il n'y a plus rien à faire).

Dans les langages de programmation impératifs, cela correspond grosso modo à l'attribution à une variable d'une nouvelle valeur, calculée à partir de l'ancienne.

Un peu sur les décors

Comme vous le comprenez, la position du chat est modélisée par une variable avec l'ensemble de toutes les pièces possibles, et non une pièce spécifique, comme ce serait le cas dans un système de simulation. L'utilisation de l'ensemble des valeurs possibles au lieu d'une valeur spécifique est une technique fréquemment utilisée dans les méthodes formelles, ce qui pose des problèmes aux programmeurs débutants. Par conséquent, j'ai choisi une tâche où l'utilisation d'ensembles est appropriée.

Structure du programme dans TLA +

Dans le cas le plus simple, le programme se compose de déclarations et d'instructions (prédicats) décrivant l'état initial, la relation entre l'état actuel et l'état suivant, et l'invariant qui doit être exécuté dans tous les états disponibles. Des prédicats auxiliaires peuvent également être présents. Les prédicats peuvent être paramétrés.

 ---- MODULE cat ------------------------------------------------------------- EXTENDS Integers CONSTANTS Doors VARIABLES CatDistr, LastDoor Init == /\ CatDistr = 0..Doors /\ LastDoor = -1 OpenDoor(n) == /\ CatDistr' = 0..Doors \intersect UNION { {x-1, x+1} : x \in CatDistr \ {n} } /\ LastDoor' = n Next == \E door \in 0..Doors : OpenDoor(door) CatWalk == CatDistr /= {} ============================================================================= 

Les première et dernière lignes sont les caractéristiques de syntaxe de la déclaration de module.

== signifie "égal par définition", tandis qu'un seul = est exactement l'égalité des valeurs calculées des expressions.

Doors est une constante du modèle, elle devra être définie dans le fichier de configuration.
CatDistr - la distribution du chat dans les chambres.

La variable LastDoor, la dernière pièce vérifiée, est entrée pour la lisibilité de la sortie du programme. Pour les grands modèles, ces variables peuvent ralentir considérablement le programme en augmentant le nombre d'états analysés (puisque l'état contient désormais un historique de son apparition et que les mêmes états créés de différentes manières seront désormais différents).

Le prédicat Init décrit l'état initial (0..Doors est l'ensemble de toutes les pièces). OpenDoor (n) décrit ce qui se passe lorsque vous ouvrez la porte de la chambre n (dans le pire des cas, le chat n'est pas là - sinon nous l'avons attrapé).

Le prédicat suivant semble un peu étrange - il y a une pièce à examiner. Le fait est que l'existence de quelque chose signifie que TLA + ne sait pas dans quelle pièce nous allons examiner, par conséquent, il vérifiera l'exactitude de l'invariant dans tous les cas.

Il serait plus clair d'écrire

 Next == OpenDoor(0) \/ OpenDoor(1) \/ ... \/ OpenDoor(Doors) 

mais alors notre code ne fonctionnera qu'avec un nombre fixe de pièces, et il vaut mieux le paramétrer.

Enfin, l'invariant CatWalk est un grand nombre de pièces où le chat peut ne pas être vide. La violation de l'invariant signifie que le chat a été attrapé, où qu'il se trouve à l'origine. Lors de la vérification de la spécification, la violation de l'invariant signifie une erreur, mais nous n'utilisons pas l'outil à sa destination et «l'erreur» trouvée signifie résoudre le problème.

Configuration du modèle

 CONSTANTS Doors = 6 INIT Init NEXT Next INVARIANT CatWalk 

Ici, tout est simple - nous avons indiqué le nombre de pièces, les conditions initiales, les conditions de changement d'état et l'invariant testé.

Le modèle est lancé à partir de la ligne de commande tlc2 -config cat.cfg cat.tla .

TLA + dispose d'une interface graphique avancée lancée par l'équipe tla-toolbox. Malheureusement, il ne comprend pas les fichiers .cfg et les paramètres du modèle devront être configurés via le menu.

Conclusion

Dans cette tâche, tout s'est avéré assez simple. Bien sûr, des cas pratiquement significatifs d'application de méthodes formelles nécessiteront des modèles beaucoup plus volumineux et l'utilisation de diverses constructions linguistiques. Mais j'espère que la résolution de ces énigmes fournira un moyen simple et non ennuyeux d'introduire des méthodes formelles dans les projets de travail.

→ La tâche a été trouvée ici

Au cas où, un programme simple pour la vérification interactive de la solution . Matériaux pour l' étude de TLA + . Un autre système de vérification des modèles, Alloy, est décrit ici .