Effectivement, pour prouver qu'un programme fait bien ce qu'on veut qu'il fasse (la correction) il faut bien commencer par savoir ce qu'on veut qu'il fasse ... Et que la machine le sache aussi. Il faut commencer par écrire les spécifiactions du programme, formellement (en B ou Coq par exemple).
Un autre problème étant de s'assurer que les specs sont elles mêmes correctes :)
Sinon pour la preuve semi-automatique, c'est vrai en B par exemple, qui à si je me souviens bien du mal à prouver des propriétés dès qu'on touche à des cardinalités d'ensemble si je me souviens bien, sachant que B est un langage de spec ensembliste. Il faut ajouter des lemmes pour aider le prouveur si besoin.
Warning aussi, mes connaissances en spec formelles se résument à des cours de B en DUT :)
[^] # Re: [X] : C'est exactement ce que j'espérais
Posté par thoasm . En réponse au journal Sondage Java sous GPL, donnez votre avis à Sun. Évalué à 2.
Un autre problème étant de s'assurer que les specs sont elles mêmes correctes :)
Sinon pour la preuve semi-automatique, c'est vrai en B par exemple, qui à si je me souviens bien du mal à prouver des propriétés dès qu'on touche à des cardinalités d'ensemble si je me souviens bien, sachant que B est un langage de spec ensembliste. Il faut ajouter des lemmes pour aider le prouveur si besoin.
Warning aussi, mes connaissances en spec formelles se résument à des cours de B en DUT :)