Δ-Extension of algebraic specification

Kazuki Yoshida, Akihiko Ohsuga, Morio Nagata, Shinichi Honiden

研究成果: Article査読

1 被引用数 (Scopus)

抄録

This paper introduces implication and a particular symbol Δ into Algebraic Specification. Implications are used in the specification as conditional equations to simplify writing axioms of a complicated requirement. With respect to Δ, there are two ways of using this symbol. (1) As a symbol to specify the partiality of an operation in axioms. Substituting Δ for the annoying description of an exceptional behavior is a particular example of this. (2) As a symbol to mean temporarily undefined in the correspondence of operations in stepwise refinement. This can make it easy to refine a part of the specification and validate it by term rewriting system. Next, a new sound and complete calculus is defined to guarantee logical consistency between implication and Δ. We can use this calculus to verify the correctness of stepwise refinement.

本文言語English
ページ(範囲)177-186
ページ数10
ジャーナルJournal of information processing
15
2
出版ステータスPublished - 1992 12 1
外部発表はい

ASJC Scopus subject areas

  • Computer Science(all)

フィンガープリント 「Δ-Extension of algebraic specification」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル