Δ-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

Specifications
Acoustic waves

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.

Δ-Extension of algebraic specification. / Yoshida, Kazuki; Ohsuga, Akihiko; Nagata, Morio; Honiden, Shinichi.

In: Journal of Information Processing, Vol. 15, No. 2, 01.12.1992, p. 177-186.

Research output: Contribution to journalArticle

Yoshida, K, Ohsuga, A, Nagata, M & Honiden, S 1992, 'Δ-Extension of algebraic specification', Journal of Information Processing, vol. 15, no. 2, pp. 177-186.
Yoshida K, Ohsuga A, Nagata M, Honiden S. Δ-Extension of algebraic specification. Journal of Information Processing. 1992 Dec 1;15(2):177-186.
Yoshida, Kazuki ; Ohsuga, Akihiko ; Nagata, Morio ; Honiden, Shinichi. / Δ-Extension of algebraic specification. In: Journal of Information Processing. 1992 ; Vol. 15, No. 2. pp. 177-186.
@article{d2fa59c90e6d4718a20a5d3ca7110297,
title = "Δ-Extension of algebraic specification",
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.",
author = "Kazuki Yoshida and Akihiko Ohsuga and Morio Nagata and Shinichi Honiden",
year = "1992",
month = "12",
day = "1",
language = "English",
volume = "15",
pages = "177--186",
journal = "Journal of Information Processing",
issn = "0387-5806",
publisher = "Information Processing Society of Japan",
number = "2",

}

TY - JOUR

T1 - Δ-Extension of algebraic specification

AU - Yoshida, Kazuki

AU - Ohsuga, Akihiko

AU - Nagata, Morio

AU - Honiden, Shinichi

PY - 1992/12/1

Y1 - 1992/12/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0027001356&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0027001356&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0027001356

VL - 15

SP - 177

EP - 186

JO - Journal of Information Processing

JF - Journal of Information Processing

SN - 0387-5806

IS - 2

ER -