http://swrc.ontoware.org/ontology#Article
Δ-extension of Algebraic Specification
en
Toshiba Corporation Systems & Software Engineering Laboratory
Toshiba Corporation Systems & Software Engineering Laboratory
Department of Administration Engineering Faculty of Science and Technology Keio University
Toshiba Corporat
Kazuki Yoshida
Akihiko Ohsuga
Morio Nagata
Shinichi Honiden
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 specifiy 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.
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 specifiy 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.
AA00700121
Journal of Information Processing
15
2
177-186
1992-10-31
1882-6652