Voltar
Artigo Acesso aberto Produção Nacional
BIBTEX RIS

Supporting ArcAngel in ProofPower

2009; Elsevier BV; Volume: 259; Linguagem: Inglês

10.1016/j.entcs.2009.12.027

ISSN

1571-0661

Autores

Frank Zeyda, Marcel Oliveira, Ana Cavalcanti,

Tópico(s)

Software Engineering Research

Resumo

ArcAngel is a specialised tactic language devised to facilitate and automate program developments using Morgan's refinement calculus. It is especially well-suited for the specification of high-level strategies to derive programs by construction, and equipped with a formal semantics that enables reasoning about tactics. In this paper, we present an implementation of ArcAngel for the ProofPower theorem prover. We discuss the underlying design, explain how it implements the semantics of ArcAngel, and examine differences in expressiveness and flexibility in comparison to ProofPower's in-built tactic language. ArcAngel supports backtracking through angelic choice; this is beyond the basic capabilities of ProofPower and many other main-stream theorem provers. The implementation is demonstrated with a non-trivial tactic example.

Referência(s)