Pourquoi les programmes ne peuvent-ils pas être prouvés?

Question

Pourquoi pas un programme d'ordinateur être prouvé comme un rapport mathématique? Une preuve mathématique est construit sur d'autres preuves, qui sont construits à partir encore plus de preuves et jusqu'aux axiomes, des vérités vérités que nous détenons comme allant de soi.

Les programmes d'ordinateur ne semblent pas disposer d'une telle structure. Si vous écrivez un programme d'ordinateur, comment est-ce que vous pouvez prendre précédente prouvé œuvres et de les utiliser pour montrer la vérité de votre programme? Vous ne pouvez pas car il n'en existe aucun. En outre, ce sont les axiomes de la programmation? La très atomique vérités du champ?

Je n'ai pas de bonnes réponses à la ci-dessus. Mais il semble que le logiciel ne peut pas être prouvé, car c'est de l'art et non de la science. Comment voulez-vous prouver un Picasso?

Answer 1

Les épreuves sont des programmes.

Vérification formelle des programmes est un vaste domaine de recherche. (Voir, par exemple, le groupe de l'université Carnegie Mellon.)

De nombreux programmes complexes ont été vérifiés; voir, par exemple, ce noyau écrit en Haskell.

Answer 2

Clairement, vous n'avez pas assez lu assez. Les programmes absolument peut être avérée correcte. Moche programmes sont difficiles à prouver. Pour le faire, même raisonnablement bien, vous avez à faire évoluer le programme et la preuve de main en main.

Vous ne pouvez pas automatiser la preuve en raison du problème de l'arrêt. Vous pouvez, cependant, manuellement prouver les post-conditions et les conditions préalables de tout arbitraire de la déclaration, ou d'une séquence d'instructions.

Vous devez lire Dijsktra est Une Discipline de Programmation.

Ensuite, vous devez lire Gries' la Science de La Programmation.

Ensuite, vous saurez comment prouver des programmes corrects.

Answer 3

Le problème d'arrêt montre seulement qu'il existe des programmes qui ne peuvent pas être vérifiés. Une question beaucoup plus intéressante et plus pratique est de savoir quelle classe de programmes peut être formellement vérifiée. Peut-être que tous les programmes qui intéressent pourraient (en théorie) être vérifiés. En pratique, jusqu'à présent, seuls les très petits programmes se sont avérés corrects.

Answer 4

Juste un petit commentaire pour ceux qui ont fait jusqu'incomplétude, ce n'est pas le cas pour tous les systèmes axiomatiques, seuls suffisamment puissant .

En d'autres termes, Gödel a prouvé qu'un système axiomatique assez puissant pour décrire lui-même serait nécessairement incomplète. Cela ne veut pas dire qu'il serait inutile toutefois, et comme d'autres l'ont lié à plusieurs tentatives de programme de preuves ont été apportées.

Le problème dual (l'écriture de programmes pour vérifier les preuves) est également très intéressante.

Answer 5

Vous pouvez en fait écrire prouvable de programmes corrects. Microsoft, par exemple, a créé une extension du langage C# appelé Spec# qui comprend un prouveur automatique. Pour java, il n'y a ESC/java. Je suis sûr qu'il y a de nombreux autres exemples.

(edit: apparemment spec# n'est plus développé, mais le contrat d'outils va devenir une partie de .NET 4.0)

Je vois des affiches à la main en agitant sur le problème de l'arrêt ou de l'incomplétude des théorèmes qui sont censées empêcher la vérification automatique de programmes. Bien sûr ce n'est pas vrai; ces questions nous dise simplement qu'il est possible d'écrire des programmes qui ne peut pas être prouvée pour être correcte ou incorrecte. Cela ne nous empêche pas de construire des programmes qui sont sensiblement correcte.