An Institution for Imperative RSL Specifications
The RAISE Specification Language (RSL) is a wide-spectrum specification language having a very complex semantics. This paper defines an institution for an imperative subset RSL I of RSL such that this subset can be given a much simpler semantics in terms of that institution. The subset allows model-oriented type definitions, declaration of state variables, axiomatic specification of values (including functions), and explicit function definitions. Functions may be imperative. The semantics of an RSL I specification is defined to be the loose semantics of a theory presentation consisting of a signature Σ and a set of sentences E that can easily be derived from the specification.
KeywordsInstitutions formal specification languages RSL algebraic semantics state based specifications
Unable to display preview. Download preview PDF.
- 4.Diaconescu, R., Futatsugi, K.: CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification. AMAST Series in Computing. World Scientific Publishing (1998)Google Scholar
- 6.Fitzgerald, J., Larsen, P.G.: Modelling Systems: Practical Tools and Techniques for Software Development, 2nd edn. Cambridge University Press (2009)Google Scholar
- 7.Goguen, J.A., Burstall, R.M.: Institutions: Abstract Model Theory for Specification and Programming. Logic of Programs 1983 39, 95–146 (1992); Predecessor in: LNCS vol. 164, pp. 221–256 (1984)Google Scholar
- 9.Jørgensen, T.D.: Transformation of Applicative Specifications into Imperative Specifications. IMM-Thesis-2005-30, Informatics and Mathematical Modelling. Technical University of Denmark, DTU, Richard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby, Supervised by Associate Professor. Ph.D. Anne E. Haxthausen and Associate Professor Hans Bruun (2004)Google Scholar
- 10.Lindegaard, M.P.: Proof Support for RAISE – by a Reuse Approach Based on Institutions. IMM-PHD-2004-132, Informatics and Mathematical Modelling. Technical University of Denmark, DTU, Richard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby, Supervised by Assoc. Prof. Anne E. Haxthausen (2004)Google Scholar
- 12.Milne, R.E.: Semantic Foundations of RSL. Technical Report RAISE/CRI/DOC/4/V1, CRI A/S (1990)Google Scholar
- 15.The RAISE Language Group. The RAISE Specification Language. The BCS Practitioners Series. Prentice Hall Int. (1992)Google Scholar
- 16.The RAISE Method Group. The RAISE Development Method. The BCS Practitioners Series. Prentice Hall Int. (1995)Google Scholar