@MASTERSTHESIS\{IMM2005-03877,
    author       = "T. D. J{\o}rgensen",
    title        = "Transformation of applicative specifications into imperative specifications",
    year         = "2005",
    keywords     = "{RAISE,} {RSL,} tool, transformation, applicative, imperative",
    school       = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}",
    address      = "Richard Petersens Plads, Building 321, {DK-}2800 Kgs. Lyngby",
    type         = "",
    note         = "Supervised by assoc. prof. Anne Haxthausen, and assoc. prof. Hans Bruun",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/3877-full.html",
    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."
}