Proof method for correctness of refinements of algebraic specification in abstract sequential machine style

In this paper, new methods for providing the correctness of refinement among abstract sequential machine style programs are described. The programs are described in algebraic language ASL using some useful notions, i.e., the extended projection and the valid reachability condition for each transition function. These notions allow a designer to refine a given text (program or specification) to a concrete text more freely than the text that does not use such notions. These notions can also enhance the expressive power of the text. On the other hand, these advantages would have lost half their values, if useful methods to prove the correctness of refinement among the texts using them are not found. Thus new methods for proving the correctness of the texts are proposed, and they do not require much proof loads. First the correctness of refinement among the ASL texts with the extended projection is defined. Second, a method is proposed for proving the correctness of refinement among such texts. Also proposed is a definition of the correctness of refinement among the texts with the valid reachability conditions and a method to prove their correctness. These methods do not require more proof loads than the usual methods for the texts that do not use such notions in the abstract sequential machine style. Therefore, these methods are useful.