The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.02 - February (1987 vol.13)
pp: 184-201
D.M. Berry , SDC, A Burroughs Company, Santa Monica, CA. 90405, and the Department of Computer Science, University of California
ABSTRACT
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. It describes the state as defined by the front matter, computations as defined by initial states and transforms, and invariants, criteria, and constraints as properties of computations. 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.
INDEX TERMS
verification, Abstract machine, correctness, formal specification, invariants, refinement methods, simulation
CITATION
D.M. Berry, "Towards a Formal Basis for the Formal Development Method and the Ina Jo Specification Language", IEEE Transactions on Software Engineering, vol.13, no. 2, pp. 184-201, February 1987, doi:10.1109/TSE.1987.232891
19 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool