||Transformation of applicative specifications into imperative specifications
||Jørgensen, Tine Damkjær
||Haxthausen, Anne Elisabeth (Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Bruun, Hans (Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
||Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
||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.
||Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU : DK-2800 Kgs. Lyngby, Denmark
||RAISE; RSL; tool; transformation; applicative; imperative
Creation date: 2006-06-22
Update date: 2012-12-19