1. Exemple de développement en Coq : preuve de correction d’un algorithme simple
La preuve de correction d’un programme fonctionnel simple nous permet de présenter quelques aspects essentiels du logiciel Coq : énoncés mathématiques et spécification formelle de programmes, outils pour la preuve interactive, etc. L’exemple proposé consiste en la définition d’une fonction de tri sur les listes, accompagnée d’une preuve formelle de sa correction.
-
Conventions typographiques
Nous adoptons les conventions suivantes afin que le lecteur puisse facilement reconnaître quel texte un utilisateur doit soumettre à Coq et quelles sont les réponses du système.
Le texte soumis à Coq est écrit dans des encarts bleu clair.
Les réponses de Coq sont présentées en italique dans des encarts cyannés.
Les expressions composées placées dans le texte de l’article sont entourées de parenthèses, comme...
Cet article est réservé aux abonnés. Il vous reste 92 % à découvrir.
Déjà abonné ? Se connecter
Exemple de développement en Coq : preuve de correction d’un algorithme simple
Applications principales
Sources bibliographiques
- (1) - - The CompCert compiler. http://compcert.inria.fr.
- (2) - - OCaml page. http://www.ocaml.org/. ...
Cet article est réservé aux abonnés. Il vous reste 92 % à découvrir.
Déjà abonné ? Se connecter
Article inclus dans l'offre
"Technologies logicielles Architectures des systèmes"
(
408 articles
)
Actualisée et enrichie d’articles validés par nos comités scientifiques.
Quiz, médias, tableaux, formules, vidéos, etc.
Opérationnels et didactiques, pour garantir l'acquisition des compétences transverses.
Un ensemble de services exclusifs en complément des ressources.
