De nombreux programmeurs ont du mal à utiliser des méthodes formelles pour résoudre des problèmes au sein de leurs programmes, car ces méthodes, bien qu'efficaces, peuvent être déraisonnablement complexes. Pour comprendre pourquoi cela se produit, utilisons la
méthode de vérification du
modèle pour résoudre un casse-tête relativement simple:
Les conditions
Vous êtes dans un couloir avec sept portes d'un côté menant à sept chambres. Un chat se cache dans l'une de ces pièces. Votre tâche consiste à attraper le chat. L'ouverture d'une porte prend une étape. Si vous devinez la bonne porte, vous attrapez le chat. Si vous ne devinez pas la bonne porte, le chat court dans la pièce voisine.
TLA + et logique temporelle
Certains outils peuvent résoudre des problèmes comme celui-ci. Par exemple, les
solveurs SMT , qui sont fréquemment utilisés dans ces cas, utilisent une logique de prédicat pour résoudre le problème, mais cela nécessite l'utilisation d'un tableau, ce qui n'est pas pratique pour les programmeurs et se traduit souvent par une séquence d'actions inutilement complexe.
TLA + , d'autre part, utilise une logique temporelle, qui permet à un programme d'utiliser l'état du système à la fois à l'étape actuelle et à l'étape suivante dans une seule instruction.
CatDistr' = CatDistr \ {n}
Cette condition stipule qu'après vérification derrière la porte N, le nombre de portes où le chat peut être localisé, coïncide avec l'ensemble des pièces d'où N a été prélevé. (Si le chat était derrière la porte N, bien sûr, il a été attrapé.)
Dans un langage de programmation impératif, cela crée une nouvelle variable calculée à partir de l'ancienne.
À propos des ensembles
La position du chat est déterminée par une variable dans l'ensemble de toutes les pièces possibles, plutôt que par une pièce spécifique comme dans un système de modélisation par simulation. Les méthodes formelles de programmation prennent en compte la pluralité de valeurs possibles, au lieu de la valeur actuelle. C'est souvent trop complexe pour les développeurs débutants, donc simplifier ce système les aiderait à travailler plus rapidement.
Structure du programme en TLA +
Le programme se compose de déclarations et de déclarations (prédicteurs), qui décrivent:
- L'état initial
- Le lien entre les états réels
- Le prochain état
- Un invariant qui s'exécute dans tous les états disponibles.
Il peut également y avoir des prédicats auxiliaires (par exemple des paramètres) impliqué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 /= {} =============================================================================
Dans cet exemple:
Configuration du modèle
CONSTANTS Doors = 6 INIT Init NEXT Next INVARIANT CatWalk
Cette configuration comprend la condition initiale, le nombre de pièces, les conditions d'un changement d'état et un test vérifiable.
Vous pouvez exécuter ce modèle à partir de la ligne de commande à l'aide de cette commande:
tlc2 -config cat.cfg cat.tla .
TLA + possède une interface graphique avancée et est lancé par la commande
tla-toolbox . Malheureusement, il ne comprend pas les fichiers
.cfg , les paramètres du modèle doivent donc être configurés via le menu.
Conclusion
La création de ce programme particulier était assez simple, mais dans de nombreux cas, l'application de méthodes formelles nécessitera des modèles beaucoup plus grands et l'utilisation de diverses constructions de langage. Nous espérons que la résolution d'énigmes plus simples comme celle-ci fournira un moyen facile et intéressant d'appliquer des méthodes formelles aux projets de travail.
- Un programme simple pour la vérification interactive de la solution peut être trouvé ici .
- En savoir plus sur TLA + ici .