ArcAngel: a Tactic Language for Refinement and its Tool Support

Oliveira, Marcel V. M. (2002) ArcAngel: a Tactic Language for Refinement and its Tool Support. Other masters thesis, Centro de Informatica, Universidade Federal de Pernambuco, Brazil. (Full text available)

PDF
Download (1MB)
[img]
Preview

Abstract

Morgan's refinement calculus is a successful technique to develop and implement software in a precise, complete, and consistent way. From a formal specification we produce a program which correctly implements the specification by repeatedly applying transformation rules, which are called refinement laws. Using the refinement calculus, however, can be a hard task, as program developments may prove to be long and repetitive. Frequently used strategies of development are reflected in sequences of law applications that are over and over applied in different developments or even in different points of a single development. A lot is to be gained from identifying these tactics of development, documenting them, and using them in program developments as a single transformation rule. In this work we present ArcAngel , a language for the definition of refinement tactics based on Angel, and formalize its semantics. Angel is a general-purpose tactic language that assumes only that rules transform proof goals. The semantics of ArcAngel is similar to Angel's semantics, but is elaborated to take into account the particularities of the refinement calculus. Most of Angel's algebraic laws are not proved. In this work we present their proofs based on the ArcAngel semantics. A normal form is also presented in this work; it is similar to that presented for Angel tactics. Our contribution in this respect is to give more details on the proofs of the lemmas and theorems involved in the strategy of reduction to this normal form. The constructs of ArcAngel are similar to those of Angel, but are adapted to deal with refinement laws and programs. Moreover, ArcAngel provides structural combinators that are suitable to apply refinement laws to components of programs. Using ArcAngel, we define refinement tactics that embody common development and programming strategies. Finally, we present Gabriel, a tool support for ArcAngel. Gabriel works as a plug-in to Refine, a tool that semi-automatizes transformations from formal specifications to correct programs with successive refinement laws applications. Gabriel allows its users to create tactics and use them in a program development.

Item Type: Thesis (Other masters)
Uncontrolled keywords: Program development, refinement calculus, tool support
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 17:59
Last Modified: 23 Jun 2014 13:45
Resource URI: http://kar.kent.ac.uk/id/eprint/13695 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year