La preuve de programme

Dix grammes d'abstraction valent des tonnes de bricolage. J.P. Rosen

Je n'ai qu'une petite tête, et il faut bien que je vive avec. C.A.R. Hoare

Des méthodes formelles existent pour exprimer la fonction d'un programme et prouver que le programme proposé réalise effectivement cette fonction.

Ces méthodes se sont généralement pas applicables à n'importe quel programme a posteriori, mais servent de guide à la conception de programmes ``prouvables''.

Il faut souligner qu'on ne sait réaliser pratiquement que la preuve de fragments de programmes relativement courts, ce qui ne constitue pas une limitation, mais plaide à nouveau pour une conception modulaire des programmes.

On ne peut qu'encourager l'emploi de techniques de preuve, qui sont enseignées dans l'unité ``algorithmique'' de seconde année.