Algebraic types and pattern matching in the logical language of the Why verification platform

Andrei Paskevich 1
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Résumé : 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.
Type de document :
Rapport
[Research Report] RR-7128, INRIA. 2009
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00439232
Contributeur : Andrei Paskevich <>
Soumis le : vendredi 28 mai 2010 - 17:59:04
Dernière modification le : jeudi 9 février 2017 - 15:51:50
Document(s) archivé(s) le : lundi 22 octobre 2012 - 12:45:44

Fichiers

RR-7128.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00439232, version 2

Collections

Citation

Andrei Paskevich. Algebraic types and pattern matching in the logical language of the Why verification platform. [Research Report] RR-7128, INRIA. 2009. 〈inria-00439232v2〉

Partager

Métriques

Consultations de la notice

248

Téléchargements de fichiers

126