In carrying out SDC’s Formal Development Method, one writes a specification of a system under design in the Ina Jo specification language and proves that the specification meets the requirements of the system. This paper develops an abstract machine model of what is specified by a level specification in an Ina Jo specification. . . . The paper then describes a number of formal design methods and the kinds of abstractions that they require. For each of these kinds of abstractions, there is a characteristic relationship between refinements that should be proved as one is carrying out the method.

--From the Author’s Abstract

The major limitation of this paper is that it is too tied up to Formal Development Method (FDM) and Ina Jo. The author assumes the reader has a reference manual “close by for reference purposes” (which I confess I did not). Eight of the 11 references are to SDC reports.

For a reader wanting an introduction to Ina Jo or a comparison with other specification languages, I would recommend the survey article [1], although it may not be entirely up to date.

There is an interesting discussion of two design methods, a “stepwise refinement” approach against a “functional enhancement” one, in Section IV of the paper. For a more formal treatment of the former, [2,3] can be suggested; I do not know of any such attempt for the latter. For another work that discusses design in a two-dimensional way see [4].