The Design And Implementation Of The Semi-automatic Aid Tool For Constructing Algebraic Specification

Formal methods are emerging as very important software development methods. Algebraic specification can be used in formal method. It used a group of algebraic axioms to describe the behaviours of operations in the given class. It provides a formal way to describe the requirement of the class more strictly. In the methodology of the class-level testing for object-oriented software based on algebraic specification, algebra specification must first be constructed as a basic condition. Axiom system is the most important part of algebraic specification. It describes the semantics of requirement. It must be with independence, consistency and integrity. This research intends to design and implement a semi-automatic tool to aid constructing algebra specification, based on the independence, integrity and consistency of algebraic specifications. It includes some local revisions to the original Scheme CLA, analysis and explanation for the reason of all possible pattens of left sides of axioms enumerated by Scheme CLA, proposing a semi-automatic approximately algorithm to validate the consistency and independence of axiom system based on the original formal definitions and propositions of the consistency and independence of the axiom system, and conducting implementations and experiments for them. These works intend to improve the efficiency of constructing algebra specification, to save the cost of formal software development, and to alleviate the difficulties of constructing axioms.