ArcAngel: a Tactic Language for Refinement and its Tool Support

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.