Modular verification of data abstractions with shared realizations

Presents a method for the modular specification and verification of data abstractions in which multiple abstract objects share a common realization level data structure. Such shared realizations are an important implementation technique for data abstractions, because they provide for efficient use of memory; i.e., they allow the amount of memory allocated to the realization of an abstract object to be dynamic, so that only the amount of memory needed for its realization is allocated to it at any one time. To be explicit, an example of this kind of data abstraction is given. Although a number of programming languages provide good support for shared realizations, there has been limited research on its specification and verification. An important property of The authors´ method is that it allows data abstractions to be dealt with modularly; i.e., each data abstraction can be specified and verified individually. Its abstract specification is made available for use by other program modules, but all of its implementation details are hidden, which simplifies the verification of code that uses the abstraction. The authors have developed semantics for data abstractions and their method of specification, and have used it to prove that their verification method is logically sound and relatively complete in the sense of Cook (1978). The use of shared realizations impacts specification and verification in several related ways. The manipulation of one abstract object may inadvertently produce a side effect on other abstract objects. Without shared realizations, such unwanted side effects can be prevented by scoping rules, but this is not possible with shared realizations. Instead, the absence of such side effects must be explicitly proven by the verification method. This requires the specification language to provide for quantification over the currently active (allocated) instances of an abstract type that is not necessary for the specification of less advanced implementations of data abstractions