Transformation of applicative specifications into imperative specifications |
| | Abstract | The RAISE Development Method is a formal software development method with an associated formal specification language, RSL, and a set of tools supporting the method and RSL.
A typical RAISE development of imperative software starts with an abstract applicative specification which is developed into a concrete applicative specification. This concrete applicative specification is then transformed into an imperative specification, which can be further developed using the RAISE Development Method.
While the development of applicative and imperative specifications is defined by a refinement relation, the transformation from applicative into imperative specification is only described informally.
This project defines a set of transformation rules, which can be used to transform an applicative RSL specification into an imperative RSL specification for a subset of RSL.
A notion of correctness of the transformation from applicative into imperative specification is defined and a verification of the correctness of the transformation rules is outlined. This means that when developing from applicative into imperative specification using the verified transformation rules, the correctness of this development step need not to be verified.
A transformation tool that implements the transformation rules has been developed. | | Keywords | RAISE, RSL, tool, transformation, applicative, imperative | | Type | Master's thesis [Academic thesis] | | Year | 2005 | | Publisher | Informatics and Mathematical Modelling, Technical University of Denmark, DTU | | Address | Richard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby | | Series | IMM-Thesis-2005-30 | | Note | Supervised by assoc. prof. Anne Haxthausen, and assoc. prof. Hans Bruun | | Electronic version(s) | [pdf] [ps] | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|