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 p rograms are described in algebraic language ASL using some useful noti ons, i.e., the extended projection and the valid reachability conditio n for each transition function. These notions allow a designer to refi ne a given text (program or specification) to a concrete text more fre ely than the text that does not use such notions. These notions can al so enhance the expressive power of the text. On the other hand, these advantages would have lost half their values, if useful methods to pro ve the correctness of refinement among the texts using them are not fo und. Thus new methods for proving the correctness of the texts are pro posed, and they do not require much proof loads. First, the correctnes s of refinement among the ASL texts with the extended projection is de fined. Second, a method is proposed for proving the correctness of ref inement among such texts. Also proposed is a definition of the correct ness of refinement among the texts with the valid reachability conditi ons and a method to prove their correctness. These methods do not requ ire 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.