Using algebraic specification languages for model-oriented specifications

Baumeister, Hubert

アイテム詳細

登録内容を編集ファイル形式で保存

一時保存へ追加

タグ情報を表示リリース履歴を表示詳細要約

公開

報告書

Using algebraic specification languages for model-oriented specifications

MPS-Authors

/persons/resource/persons44086

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

External Resource

There are no locators available

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

フルテキスト (公開)

1996-2-003
(全文テキスト（全般）), 11KB

付随資料 (公開)

There is no public supplementary material available

引用

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

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

要旨

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.