Mechanised support for sound refinement tactics

TY - JOUR

T1 - Mechanised support for sound refinement tactics

AU - Zeyda, Frank

AU - Oliveira, Marcel

AU - Cavalcanti, Ana Lucia Caneca

PY - 2012/1/1

Y1 - 2012/1/1

N2 - ArcAngel is a 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 refinement strategies, and equipped with a formal semantics that additionally permits 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 the interplay between ArcAngel tactics and the native reasoning support of the prover. We also discuss several extensions of ArcAngel that have been entailed by our implementation effort. They are of practical importance and provide a unification of the related tactic languages Angel and ArcAngelC. Our main result is a mechanisation that reflects directly the ArcAngel semantics, and can be used with any programming model for refinement. The approach can be used to support other formal tactic languages using other theorem provers.

AB - ArcAngel is a 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 refinement strategies, and equipped with a formal semantics that additionally permits 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 the interplay between ArcAngel tactics and the native reasoning support of the prover. We also discuss several extensions of ArcAngel that have been entailed by our implementation effort. They are of practical importance and provide a unification of the related tactic languages Angel and ArcAngelC. Our main result is a mechanisation that reflects directly the ArcAngel semantics, and can be used with any programming model for refinement. The approach can be used to support other formal tactic languages using other theorem provers.

UR - http://www.scopus.com/inward/record.url?scp=84856593897&partnerID=8YFLogxK

U2 - 10.1007/s00165-011-0218-z

DO - 10.1007/s00165-011-0218-z

M3 - Article

SN - 0934-5043

VL - 24

SP - 127

EP - 160

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 1

ER -