Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-I-96-2-003

Using algebraic specification languages for model-oriented specifications

Baumeister, Hubert

MPI-I-96-2-003. February 1996, 17 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
It is common belief that there is a substantial difference between model-oriented (eg. Z and VDM) and algebraic specification languages (eg. LSL and ACT-ONE) wrt. their applicability to the specification of software systems. While model-oriented specification languages are assumed to be suited better for the description of state based systems (abstract machines), algebraic specification languages are assumed to be better for abstract datatype specifications. In this paper we shall demonstrate how an algebraic specification language (the Larch Shared Language) can be used to write specifications of abstract machines in the style of Z and how support tools for algebraic specification languages, eg. type checker and theorem provers, can be used to reason about abstract machines.
Acknowledgement:
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-96-2-003.psMPI-I-96-2-003.pdf213 KBytes; 234 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1996-2-003
Hide details for BibTeXBibTeX
@TECHREPORT{Baumeister96,
  AUTHOR = {Baumeister, Hubert},
  TITLE = {Using algebraic specification languages for model-oriented specifications},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-96-2-003},
  MONTH = {February},
  YEAR = {1996},
  ISSN = {0946-011X},
}