A Functional Approach to Module Verification

The purpose of this paper is to develop a method for designing and verifying data abstractions using the functional approach. Before doing so, the existing techniques for designing and verifying procedure and data abstractions will be surveyed briefly. These techniques will then be modified and extended to verify data abstractions. By using the concept of a mathematical function, one can model the behavior of a procedure abstraction and give a more uniform and clearer meaning to the stepwise refinement and verification of procedure abstractions. The concept of a state machine is then used as a basis to specify data abstractions. Using state machine specification, a technique for expressing the design of a data abstraction is then given. A method is then developed to verify the design of a data abstraction with respect to its specifications.