Using algebraic specification languages for model-oriented specifications

Baumeister, Hubert

Datensatz

DATENSATZ AKTIONENEXPORT

Zur Ablage hinzufügen

Lokale TagsFreigabegeschichteDetailsÜbersicht

Freigegeben

Bericht

Using algebraic specification languages for model-oriented specifications

MPG-Autoren

/persons/resource/persons44086

Baumeister, Hubert
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen

Es sind keine externen Ressourcen hinterlegt

Volltexte (beschränkter Zugriff)

Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.

Volltexte (frei zugänglich)

1996-2-003
(beliebiger Volltext), 11KB

Ergänzendes Material (frei zugänglich)

Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar

Zitation

Baumeister, H.(1996). Using algebraic specification languages for model-oriented specifications (MPI-I-1996-2-003). Saarbrücken: Max-Planck-Institut für Informatik.

Zitierlink: https://hdl.handle.net/11858/00-001M-0000-0014-9FEF-5

Zusammenfassung

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.