Matita

Matita assistant de preuve expérimental en cours de développement au département d'informatique de l' université de Bologne . Il s'agit d'un outil facilitant le développement de preuves formelles par collaboration homme-machine, fournissant un environnement de programmation où les spécifications formelles , les algorithmes exécutables et les certificats de correction vérifiables automatiquement coexistent naturellement.

Matita est basé sur un système de types dépendants connu sous le nom de calcul des constructions (co)inductives (un dérivé du calcul des constructions ), et est compatible, dans une certaine mesure, avec Coq .

Le mot « matita » signifie « crayon » en italien (un outil d'édition simple et répandu). Il s'agit d'une application relativement petite et simple, dont la complexité architecturale et logicielle est destinée à être maîtrisée par les étudiants, fournissant un outil particulièrement adapté pour tester des idées et des solutions innovantes. Matita adopte un mode d'édition basé sur des tactiques ; des objets de preuve ( encodés en XML ) sont produits pour le stockage et l'échange.

Les variables existentielles sont natives dans Matita, permettant une gestion plus simple des objectifs dépendants.

Matita implémente un algorithme d'inférence de type bidirectionnel exploitant à la fois les types inférés et attendus.

La puissance du système d'inférence de type (raffineur) est encore augmentée par un mécanisme d'indices qui aide à synthétiser des unificateurs dans des situations particulières spécifiées par l'utilisateur.

Matita prend en charge une stratégie de désambiguïsation sophistiquée basée sur un dialogue entre l' analyseur et le vérificateur de types .

Au niveau interactif, le système implémente une exécution en petites étapes de tactiques structurées permettant une bien meilleure gestion du développement de la preuve, et conduisant naturellement à des scripts plus structurés et lisibles.

Matita a été employée dans CerCo (Certified Complexity) : un projet européen FP7 axé sur le développement d'un compilateur formellement vérifié et préservant la complexité d'un grand sous-ensemble de C vers le langage assembleur d'un microprocesseur MCS-51 .

Le tutoriel Matita fournit une introduction pragmatique aux principales fonctionnalités du démonstrateur de théorèmes interactif Matita, offrant une visite guidée à travers un ensemble d'exemples non triviaux dans le domaine de la spécification et de la vérification de logiciels .