L’utilité de cette logique est triple :
- Un programme étant donné, démontrer qu’il implémente bien l’algorithme représenté ;
- Un programme étant donné, deviner quel algorithme il implémente ;
- Un algorithme étant donné, construire un programme correct.
Chacune de ces tâches est susceptible d’être elle-même informatisée, ce qui donne lieu à des logiciels analysant ou construisant des algorithmes. Un exemple dans la langue de Goethe.
L’objet de l’article ci-dessous est une liste d’exemples illustrant comment la logique de Hoare fonctionne, en l’ocurrence sur des exemples de la classe de Seconde. Les exemples sont rédigés en JavaScript, avec un code de couleurs qui devrait, pour les lecteurs non daltoniens, faciliter la lecture. Pour autant le sujet n’est pas vraiment facile...
Il est à remarquer que la logique de Hoare achoppe sur des sujets tels que la récursivité et le calcul parallèle, qui par un étrange hasard, sont hors du programme du lycée...
Le pdf ci-dessous est placé sous license « creative commons » : Vous avez le droit de le lire (youpi !) et de le diffuser ; vous avez même le droit de le modifier (c’est d’ailleurs le but du choix de cette license). La seule chose dont vous n’avez pas le droit, c’est de prétendre en être l’auteur (!).
This work is in the Public Domain.
Mercredi 12 septembre 2012, 14h-17h30, salle S23.6 du Parc technologique universitaire (Saint-Denis)
Commentaires