[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php

Bibliographic Item (1.0)

ErnstHookwayOgden94

  1. George W Ernst & Raymond J Hookway & William F Ogden
  2. Modular Verification of Data Abstractions with Shared Realizations
  3. IEEE Trans SE-30n4(Apr 1994)pp288-307
      Note ADTs export types modula RESOLVE From Abstract: "The abscence of 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"

      Abstraction is a mixture of code and specification

      invariant, require, and ensure assertions

      Automatic initializations

      IntegerSet example

      Quantification for Q x:1..alloc( ... R[x] ....) Variable x (an object of exported type) is replaced by R[x] inside. Assume and Confirm statements MetaTheory ??Lamport/Lam Shankar?? ->p304: "A valid program is a collection of valid modules in which each item imported by a module is exported by precisely one other module, and in which the specs of imported and exported items are compatible"



Search for bibliographic items containing a matching string.


(Search uses POSIX regular expressions and ignores case)

Search for a specific bibliographic item by name.



To see the complete bibliography (1Mb+) select:[Bibliography]