### 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 language | English |
---|---|

Pages (from-to) | 177-186 |

Number of pages | 10 |

Journal | Journal of Information Processing |

Volume | 15 |

Issue number | 2 |

Publication status | Published - 1992 Dec 1 |

Externally published | Yes |

### Fingerprint

### ASJC Scopus subject areas

- Engineering(all)

### Cite this

*Journal of Information Processing*,

*15*(2), 177-186.

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

Research output: Contribution to journal › Article

*Journal of Information Processing*, vol. 15, no. 2, pp. 177-186.

}

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 -