Bonjour,
N'y connaissant pas grand chose en preuve formelle, je cherche à m'exercer sur un exemple (un petit programme style résolution de sudoku). J'avais essayé OCaml et Haskell il y a 3 ans mais je ne me souviens plus très bien de la syntaxe.
Donc j'aimerais avoir votre avis sur le langage le plus adapté pour transformer une spécification algébrique en programme (et inversement , un programme en spéc), puis de faire la preuve de la spéc (avec un arbre de preuve, en utilisant les axiomes, la réflexion, la symétrie, la transitivité, la congruence, ...).
Ca ne dépend pas du langage, mais j'aimerais aussi utiliser un peu des outils d'aide à la preuve, qui font pour nous les étapes les plus faciles comme la symétrie ou la transitivité.
Pour info, voici la spécification algébrique des entiers naturels et de l'addition :
Je vous remercie pour votre aide.
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17 Sortes : Nat Constructeurs : 0 : -> Nat plusUn : Nat -> Nat Fonctions : plus : Nat * Nat -> Nat Axiomes : plus(x, 0) = x plus(x, plusUn(y)) = plus(plusUn(x), y) Variables : x : Nat y : Nat
Partager