Séminaire APRRSS

Développement de programmes impératifs par raffinements, au sein de l'assistant de preuves Coq

31/05/2018
Intervenant(s) : Boubacar Sall (APR)
D'une spécification abstraite intelligible à un programme éfficace, il peut exister un écart important. Cet écart est en général difficile à combler d'une traite. La technique des raffinements successifs est un moyen de répondre à ce problème. Il s'agit d'appliquer à la spécification initiale une séries de transformations simples, qui permettent après chaque transformation de se rapprocher d’une solution exécutable. La correction du programme finalement obtenu découle alors de la correction des transformations, correction dont il faut bien entendu s'assurer, par la preuve de préférence. Dans ce séminaire, nous présentons une application du raffinement qui s'appuie sur l'assistant de preuves Coq afin de formaliser les spécifications, les programmes, la méthodologie de raffinement ainsi que les obligations de preuves qui en découlent.

romain.demangeon (at) nulllip6.fr
Mentions légales
Carte du site