Advertisement

An Institution for Imperative RSL Specifications

  • Anne E. Haxthausen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8373)

Abstract

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.

Keywords

Institutions formal specification languages RSL algebraic semantics state based specifications 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Baumeister, H., Zamulin, A.V.: State-Based Extension of CASL. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol. 1945, pp. 3–24. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  2. 2.
    Bolignano, D., Debabi, M.: Higher Order Communicating Processes with Value-passing, Assignment and Return of Results. In: Ibaraki, T., Iwama, K., Yamashita, M., Inagaki, Y., Nishizeki, T. (eds.) ISAAC 1992. LNCS, vol. 650, pp. 319–331. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  3. 3.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)zbMATHGoogle Scholar
  4. 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
  5. 5.
    Diaconescu, R., Futatsugi, K., Ogata, K.: CafeOBJ: Logical Foundations and Methodologies. Computing and Informatics 22, 257–283 (2003)MathSciNetzbMATHGoogle Scholar
  6. 6.
    Fitzgerald, J., Larsen, P.G.: Modelling Systems: Practical Tools and Techniques for Software Development, 2nd edn. Cambridge University Press (2009)Google Scholar
  7. 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
  8. 8.
    Hennicker, R., Bidoit, M.: Observational Logic. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp. 263–277. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  9. 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. 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
  11. 11.
    Lindegaard, M.P., Haxthausen, A.E.: Proof Support for RAISE – by a Reuse Approach based on Institutions. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 319–333. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  12. 12.
    Milne, R.E.: Semantic Foundations of RSL. Technical Report RAISE/CRI/DOC/4/V1, CRI A/S (1990)Google Scholar
  13. 13.
    Mossakowski, T., Haxthausen, A., Sannella, D., Tarlecki, A.: Casl, the Common Algebraic Specification Language: Semantics and proof theory. Computing and Informatics 22(3-4), 285–322 (2003)MathSciNetzbMATHGoogle Scholar
  14. 14.
    Mosses, P.D. (ed.): CASL Reference Manual. LNCS, vol. 2960. Springer, Heidelberg (2004)zbMATHGoogle Scholar
  15. 15.
    The RAISE Language Group. The RAISE Specification Language. The BCS Practitioners Series. Prentice Hall Int. (1992)Google Scholar
  16. 16.
    The RAISE Method Group. The RAISE Development Method. The BCS Practitioners Series. Prentice Hall Int. (1995)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Anne E. Haxthausen
    • 1
  1. 1.DTU ComputeTechnical University of DenmarkKgs. LyngbyDenmark

Personalised recommendations