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

## ASJC Scopus subject areas

- Computer Science(all)