Δ-Extension of algebraic specification

Kazuki Yoshida, Akihiko Ohsuga, Morio Nagata, Shinichi Honiden

Research output: Contribution to journalArticle

1 Citation (Scopus)

Abstract

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.

Original languageEnglish
Pages (from-to)177-186
Number of pages10
JournalJournal of Information Processing
Volume15
Issue number2
Publication statusPublished - 1992 Dec 1
Externally publishedYes

    Fingerprint

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Yoshida, K., Ohsuga, A., Nagata, M., & Honiden, S. (1992). Δ-Extension of algebraic specification. Journal of Information Processing, 15(2), 177-186.