A theory for program and data type specification (Q1199933)

This is an attempt to develop a wide spectrum formalism which will support not only reasoning about program equivalence, but also covers reasoning about some properties of computations, specifications of programs and data types. The first-order, two-layered theory which is called IOCC (impredective theory of operations, control and classes) was created for these purposes. The lower layer is a theory of program equivalence and definedness. The upper layer is a theory of class membership with a general principle for defining classes. Examples are given to illustrate the reasoning about programs, steams and coroutines.