Introduction

Des ressources pédagogiques utilisées pour enseigner la vérification de programmes aux scientifiques et ingénieurs sont désormais disponibles. elles comprennent des diapositives de cours et des exercices avec solutions.

Si l’apprentissage de Dafny et de la vérification de programmes vous intéresse, vous pouvez commencer immédiatement. Vous apprendrez à programmer en Dafny, à utiliser Dafny comme assistant de preuve et, enfin, à vérifier des programmes. Si vous êtes plutôt intéressé par l’enseignement de la vérification de programmes, l’organisation des cours et l’accent mis sur Dafny comme assistant de preuve pourraient vous surprendre. Les notes suivantes devraient fournir un contexte et des explications.

Dafny : Vérificateur de programmes et assistant de preuve

Une preuve joue deux rôles.
(i) Une preuve convainc le lecteur que l’énoncé est correct.
(ii) Une preuve explique pourquoi l’énoncé est correct.

Herman Geuvers, dans Proof assistants: History, ideas and future

Selon Herman Geuvers, une preuve a deux fonctions essentielles : convaincre de la justesse d’un énoncé et expliquer pourquoi il est correct.La première fonction implique des vérifications administratives, tandis que la seconde offre une intuition du théorème.

Une approche de l’introduction à la vérification de programmes, incluant la rédaction de spécifications et de preuves, est illustrée par le livre Program Proofs de K. Rustan M. Leino. La vérification est toujours motivée par des programmes, et les spécifications et les preuves sont des attributs des programmes. Le livre commence par des programmes impératifs simples dont la spécification est écrite sous forme de pré et post conditions, et la preuve est réalisée en écrivant des annotations pour les boucles et, occasionnellement, des assertions supplémentaires. Le concept de preuve est introduit implicitement par une logique de program qui détaille l’effet des différentes constructions de programmation sur la validité d’une spécification. Combinée à l’automatisation de Dafny,cette méthode permet de vérifier des programmes en les décorant avec quelques assertions qui expliquent à haut niveau pourquoi la spécification devrait être valide. Elle favorise un style de vérification de programmes où prouver revient à expliquer.

Cependant, lorsque l’automatisation est insuffisante, il peut être difficile de déterminer quelles explications aideront à la vérification. Il peut sembler nécessaire de fournir la bonne assertion au bon endroit, sans méthodologie claire. Pour résoudre ce problème, une viewpoint complémentaire sur la vérification de programmes en Dafny est proposée. L’idée clé est de présenter Dafny comme un assistant de preuve et d’étudier les preuves explicitement et indépendamment des programmes.Cette perspective permet d’apprendre à écrire des preuves intuitives qui tirent parti de l’automatisation, mais aussi à rédiger des preuves formelles détaillées en déduction naturelle. Cette méthodologie ouvre la possibilité de prouver en convainquant : un ensemble de règles peut être utilisé pour affiner une preuve qui finira par passer la vérification si elle est valide.

Le cours est organisé en trois parties distinctes. Dans les deux premières, Dafny est présenté comme un langage de programmation (sans vérification) et comme un assistant de preuve (sans programmation). La vérification de programmes est introduite en dernier et met l’accent sur la vérification extrinsèque.

Partie 1 : Dafny comme langage de programmation

La première série de cours présente Dafny comme un langage de programmation, sans considération pour la vérification. L’objectif principal est de permettre aux nouveaux utilisateurs de Dafny de se familiariser avec la syntaxe et la sémantique du langage, ainsi qu’avec ses outils (CLI, IDE). Cela permet également aux développeurs Dafny plus expérimentés de passer directement à la vérification. Enfin, cela souligne que Dafny est avant tout un langage de programmation à part entière, avec un typage statique fort, une orientation objet et des fonctionnalités fonctionnelles. Il peut être intéressant de présenter l’interface de fonction étrangère de Dafny et l’idée que Dafny peut être utilisé dans le cadre d’un projet logiciel de grande envergure.

Nous présentons successivement la programmation fonctionnelle, la programmation impérative et la programmation orientée objet. La présentation du système de modules est généralement réduite au minimum.

Partie 2 : Dafny comme assistant de preuve

Après avoir présenté Dafny comme un langage de programmation sans tenir compte de la vérification, nous découvrons Dafny comme un assistant de preuve sans tenir compte de la programmation.

Nous commençons par présenter le langage de spécification de Dafny.Une spécification Dafny est composée de symboles non interprétés de type, de symboles constants, de prédicats et de fonctions, et le langage des formules est une variante de la théorie des types simples de Church ou de la logique d’ordre supérieur. Le cours présente également le lemme comme un moyen de déclarer une famille de formules et d’axiomatiser la signification des symboles. En particulier, les types et opérations primitifs tels que les réels ou les ensembles sont présentés comme des théories spécifiques.

Nous expliquons ensuite comment définir des types, des constantes, des prédicats et des fonctions au lieu de les axiomatiser et de supposer leur existence. C’est l’occasion de parler de partialité, de terminaison des fonctions, de points fixes et de types de données algébriques.

Enfin, nous commençons à étudier les preuves dans Dafny de la manière la plus intuitive qui vise à prouver en expliquant. Dans ce style, qui est le style de preuve Dafny le plus idiomatique, on peut prouver d’une manière similaire au type de preuves que l’on écrit dans un cours de géométrie au lycée en faisant des assertions intermédiaires, en faisant appel à