on programming methodology. an abstraction, specifying its behavior Alphard language constructs allow a programmer to isolate publicly while localizing knowledge about its implementation. The verification of such an abstraction consists of showing that its implementation behaves in accordance with the public specification. Given such a verification, the abstraction may be used with confidence to construct higher·level, more abstract, programs. The most common kind of abstraction in Alphard corresponds to what is now called an abstract data type. An abstract data type comprises a set of values for elements of the type and a set of operations on those values. A new language construct, the form, provides a way to encapsulate the definitions of data structures and operations in such a way that only public information could be accessed by the rest of the program.