A system for the refinements of algebraic specifications and their efficient executions

The algebraic specification method is one of the promising methods for the development of reliable programs. Although the correctness of some programs has been proved by using this method, the practical verification examples and their working loads have not been investigated sufficiently. The frameworks for describing the readable specifications and the mechanisms for efficient executions should be studied further. The authors have designed an algebraic specification language ASL, and have been constructing a support system for the refinements of algebraic specifications and their efficient executions. They have described the abstract specifications for a quicksort program, vi-like screen editors, an inventory control problem and a simple CPU. These specifications have been refined to the executable programs step by step, and the correctness of the refinements has been proven by using the support system. The working loads used for the verification have been also examined. The features of the support system are summarized. The verification facilities and the efficiency of the derived programs is described