This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Towards a Formal Basis for the Formal Development Method and the Ina Jo Specification Language
February 1987 (vol. 13 no. 2)
pp. 184-201
D.M. Berry, SDC, A Burroughs Company, Santa Monica, CA. 90405, and the Department of Computer Science, University of California
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, Feb. 1987, doi:10.1109/TSE.1987.232891
Usage of this product signifies your acceptance of the Terms of Use.