Abstract
This paper presents an elementary formal approach (or rather, a catalog of definitions) which provides a general framework for non-deterministic system specification : definitions are given for a system, a halting system, abstraction and implementation, and finally for the extension and refinement of a system. The notion of an invariant function is extended to that of an almost invariant function.
In a second part, we apply this formalism to the specification of a disk handler and of a small "on-line" query system.
Preview
Unable to display preview. Download preview PDF.
References
DIJKSTRA, E.W. Guarded commands, nondeterminacy and formal derivation of programs. Comm. ACM 18, 8 (Aug. 1975)
HOARE, C.A.R. Communicating sequential processes. Comm. ACM 21,8 (Aug. 1978)
BRINCH HANSEN, P. Distributed processes: A concurrent programming concept. Comm. ACM 21,11 (Nov. 1978)
OWICKI, S. GRIES, D. An axiomatic proof technique for parallel programs. I. Acta Informatica 6 (1976)
OWICKI, S. Axiomatic proof techniques for parallel programs Dept. C.S. Cornell University TR 75–251 (1975)
HOARE, C.A.R. An axiomatic basis for computer programming Comm. ACM 12,10 (Oct. 1969)
GRIES, D. An exercise in proving parallel programs correct. Comm. ACM 20,12 (Dec. 1977)
DIJKSTRA, E.W. et al. On-the-fly garbage collection: An exercise in cooperation Comm. ACM 21,12 (Nov. 1978)
SINTZOFF, M. Inventing program construction rules in Constructing quality Software North-Holland/IFIP (1978)
MEYER, B. DEMUYNCK, M. Specification languages: A critical survey and proposal. Submitted for publication.
ABRIAL, J.R. Z: A specification language. Proceedings of the international conference on mathematical studies of information processing. Kyoto, Japan (Aug. 1978)
KURATOWSKI, K Introduction à la théorie des ensembles et à la topologie. Dunod.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1979 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abrial, J.R., Schuman, S.A. (1979). Non-deterministic system specification. In: Kahn, G. (eds) Semantics of Concurrent Computation. Lecture Notes in Computer Science, vol 70. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0022462
Download citation
DOI: https://doi.org/10.1007/BFb0022462
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-09511-8
Online ISBN: 978-3-540-35163-4
eBook Packages: Springer Book Archive