A Toolchain to Produce Correct-by-Construction OCaml Programs

Jean-Christophe Filliâtre 1 Léon Gondelman 1 Andrei Paskevich 2 Mário Pereira 3 Simão Melo de Sousa 4
2 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
3 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : This paper presents a methodology to get correct-by-construction OCaml programs using the Why3 tool. First, a formal behavioral specification is given in the form of an OCaml module signature extended with type invariants and function contracts, in the spirit of JML. Second, an implementation is written in the programming language of Why3 and then verified with respect to the specification. Finally, an OCaml program is obtained by an automated translation. Our methodology is illustrated with the proof of a union-find library. Several other proofs of data structures and algorithms are included in the companion artifact to this paper.
Type de document :
Pré-publication, Document de travail
2018
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01783851
Contributeur : Mário José Parreira Pereira <>
Soumis le : mercredi 2 mai 2018 - 17:19:56
Dernière modification le : samedi 5 mai 2018 - 01:20:47
Document(s) archivé(s) le : mardi 25 septembre 2018 - 03:42:15

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01783851, version 1

Citation

Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich, Mário Pereira, Simão Melo de Sousa. A Toolchain to Produce Correct-by-Construction OCaml Programs. 2018. 〈hal-01783851〉

Partager

Métriques

Consultations de la notice

276

Téléchargements de fichiers

199