Beta 1


Title Transformation of applicative specifications into imperative specifications
Author Jørgensen, Tine Damkjær
Supervisor 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)
Institution Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
Thesis level Master's thesis
Year 2005
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.
Imprint Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU : DK-2800 Kgs. Lyngby, Denmark
Pages 576
Keywords RAISE; RSL; tool; transformation; applicative; imperative
Fulltext
Original Postscript imm3877.ps (3.99 MB)
Derived PDF imm3877.pdf (2.50 MB)
Admin Creation date: 2006-06-22    Update date: 2012-12-19    Source: dtu    ID: 185844    Original MXD