Algebraic types and pattern matching in the logical language of the Why verification platform
Résumé
We introduce an extension of the logical language of a software verification tool Why with algebraic types and pattern matching expressions. We describe the corresponding additions to the syntax of Why and give the semantics of the new constructions in terms of first-order logic with polymorphic types as it is adopted in Why and the Alt-Ergo prover.
On introduit une extension du langage logique de l'outil de vérification des logiciels Why avec des types algébriques et des expressions de filtrage par motif. On décrit les modifications correspondantes de la syntaxe de Why et on donne la sémantique des nouvelles constructions dans la logique du premier ordre avec des type polymorphes telle qu'elle est adoptée dans Why et dans le démonstrateur automatique Alt-Ergo.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...