Title :

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

Author(s) :

Rusu, Vlad [Auteur]
Centre Inria de l'Université de Lille
Arusoaie, Andrei [Auteur]

Journal title :

Journal of Logical and Algebraic Methods in Programming

Pages :

68–91

Publisher :

Elsevier

Publication date :

2017-12

ISSN :

2352-2208

English keyword(s) :

Reachability Logic
state monad
Maude
higher-order function

HAL domain(s) :

Informatique [cs]/Logique en informatique [cs.LO]
Informatique [cs]/Langage de programmation [cs.PL]

English abstract : [en]

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 ...
Show more >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.Show less >

Language :

Anglais

Peer reviewed article :

Oui

Audience :

Internationale

Popular science :

Non

Comment :

(to appear)

Collections :

• Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL