2022-01-16T19:18:16Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:000596342017-03-31T05:36:57Z05471:05474:05478
Δ-extension of Algebraic SpecificationΔ-extension of Algebraic Specificationenghttp://id.nii.ac.jp/1001/00059634/Articlehttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=59634&item_no=1&attribute_id=1&file_no=1Copyright (c) 1992 by the Information Processing Society of JapanToshiba Corporation Systems & Software Engineering LaboratoryToshiba Corporation Systems & Software Engineering LaboratoryDepartment of Administration Engineering Faculty of Science and Technology Keio UniversityToshiba CorporatKazuki, YoshidaAkihiko, OhsugaMorio, NagataShinichi, HonidenThis 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.AA00700121Journal of Information Processing 1521771861992-10-311882-66522009-06-30