| 摘要 |
PURPOSE:To expand the application range of algebraic specification description by providing the algebraic specification describing system with a prescribed code expanding part in which formed operation is virtually defined as the whole area, an inference rule part for defining a new, sound and complete inference rule, and so on. CONSTITUTION:In the case of forming specifications based upon a user's request for system development, a user request system part 1 and an algebraic specification describing part 2 are provided. The system part 1 is provided with a multi-sort algebraic part, an undefined symbol DELTA adding part 4 and the DELTA expanding part 5 in which formed operation is virtually defined over the whole area. On the other hand, the description part 2 is provided with an equation set part 6, an addition part 4, an implication set part 7, and an inference rule part for defining a new, sound and complete inference rule at the time of leading the implication. The operation partially defined as the set is virtually to the whole area in the system part 1, the symbol expressing undefinition is added also in the description part 2 and the implication is led in to improve description performance, so that the sound and complete inference rule can be defined. Thus the application range of algebraic specification description can be expanded.
|
