Executing and Verifying Higher-Order Functional-Imperative Programs in Maude

Abstract : We incorporate higher-order functions and state monads in Maude, thereby embedding a higher-order functional language with imperative features in the Maude framework. We illustrate, via simple programs in the resulting language: the concrete and symbolic execution of programs; their verification with respect to properties expressed in Reachability Logic, a language-parametric generalisation of Hoare Logic; and the verification of program-equivalence properties. Our approach is proved sound and is implemented in Full Maude by taking advantage of its reflective features and module system.
Type de document :
Article dans une revue
Journal of Logical and Algebraic Methods in Programming, Elsevier, 2017, pp.45
Liste complète des métadonnées


https://hal.inria.fr/hal-01586341
Contributeur : Pal Dream <>
Soumis le : mardi 12 septembre 2017 - 16:33:53
Dernière modification le : jeudi 14 septembre 2017 - 01:09:13

Fichier

wrla-jlamp-R2.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01586341, version 1

Collections

Citation

Vlad Rusu, Andrei Arusoaie. Executing and Verifying Higher-Order Functional-Imperative Programs in Maude. Journal of Logical and Algebraic Methods in Programming, Elsevier, 2017, pp.45. <hal-01586341>

Partager

Métriques

Consultations de
la notice

30

Téléchargements du document

6