A Logical Framework to Prove Properties of Alpha Programs (revised version)

Luc Bougé 1 David Cachera 1
1 REMAP - Regularity and massive parallel computing
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
Abstract : We present an assertional approach to prove properties of Alpha programs. Alpha is a functional language based on affine recurrence equations. We first present two kinds of operational semantics for Alpha together with some equivalence and confluence properties of these semantics. We then present an attempt to provide Alpha with an external logical framework. We therefore define a proof method based on invariants. We focus on a particular class of invariants, namely canonical invariants, that are a logical expression of the program's semantics. We finally show that this framework is well-suited to prove partial properties, equivalence properties between Alpha programs and properties that we cannot express within the Alpha language
Type de document :
Rapport
[Research Report] RR-3177, INRIA. 1997
Liste complète des métadonnées

https://hal.inria.fr/inria-00073512
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 13:05:54
Dernière modification le : mercredi 11 avril 2018 - 01:52:52
Document(s) archivé(s) le : dimanche 4 avril 2010 - 21:59:55

Fichiers

Identifiants

  • HAL Id : inria-00073512, version 1

Citation

Luc Bougé, David Cachera. A Logical Framework to Prove Properties of Alpha Programs (revised version). [Research Report] RR-3177, INRIA. 1997. 〈inria-00073512〉

Partager

Métriques

Consultations de la notice

265

Téléchargements de fichiers

87