Abstract
The lack of expressive power of temporal logic as a specification language can be compensated to a certain extent by the introduction of powerful, high-level temporal operators, which are difficult to understand and reason about. A more natural way to increase the expressive power of a temporal specification language is by introducing conceptual state variables, which are auxiliary (unimplemented) variables whose values serve as an abstract representation of the internal state of the process being specified. The kind of specifications resulting from the latter approach are called conceptual state specifications.
This paper considers a central problem in reasoning about conceptual state specifications: the problem of proving entailment between specifications. A technique, based on the notion of simulation between machines, is shown to be sound for proving entailment. A kind of completeness result can also be shown, if specifications are assumed to satisfy certain well-formedness conditions. The role played by entailment in proofs of correctness is illustrated by the problem of proving that the concatenation of two FIFO buffers implements a FIFO buffer.
This research was supported in part by ARO grant DAAG29-84-K-0058, NSF grant DCR-83-02391, and DARPA grant N00014-82-K-0125.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
H. Barringer, R. Kuiper, “A Temporal Logic Specification Method Supporting Hierarchical Development,” Manuscript, University of Manchester Department of Computer Science, November, 1983.
H. Barringer, R. Kuiper, “Now You May Compose Temporal Specifications,” Proceedings of the Sixteenth ACM Symposium on Theory of Computing, April, 1984, pp. 51–63.
J.A. Goree, “Internal Consistency of a Distributed Transaction System with Orphan Detection,” MIT/LCS/TR-286, 1981.
J.V. Guttag, E. Horowitz, D.R. Musser, “Abstract Data Types and Software Validation,” Comm. ACM 21, 12 (Dec., 1978), pp. 1048–1064.
B.T. Hailpern, S. S. Owicki, “Verifying Network Protocols Using Temporal Logic,” Technical Report No. 192, Computer Systems Laboratory, Stanford University, June, 1980.
C.A.R. Hoare, “Proof of Correctness of Data Representations,” Acta Informatica 1, 4 (1972), pp. 271–281.
C. B. Jones, “Development Methods for Computer Programs Including a Notion of Interference,” Wolfson College, June, 1981.
L. Lamport, “'sometime’ is Sometimes ‘Not Never',” Seventh ACM Conference on Principles of Programming Languages, 1980.
L. Lamport, “Specifying Concurrent Program Modules,” ACM Transactions on Programming Languages and Systems, 5, 2 (April, 1983), pp. 190–222.
N.A. Lynch, “Concurrency Control for Resilient Nested Transactions,” ACM SIGACTSIGMOD Symposium on Principles of Database Systems, Atlanta, March, 1983.
Z. Manna, A. Pnueli, “Verification of Concurrent Programs: A Temporal Proof System,” Stanford University Report No. STAN-CS-83-967, June, 1983.
S. S. Owicki, L. Lamport, “Proving Liveness Properties of Concurrent Programs,” ACM Transactions on Programming Languages and Systems, 4, 3 (July 1982), 455–495.
A. Pnueli, “The Temporal Logic of Programs,” IEEE Symposium on Foundations of Computer Science, 1977.
R. L. Schwartz, P. M. Melliar-Smith, “Temporal Logic Specification of Distributed Systems,” Second International Conference on Distributed Systems, INRIA, France, April, 1981.
E. W. Stark, “Foundations of a Theory of Specification for Distributed Systems,” M.I.T. Laboratory for Computer Science Technical Report MIT/LCS/TR-342, August, 1984.
E. W. Stark, “Proving Entailment Between Conceptual State Specifications,” Department of Computer Science Technical Report 85/15, State University of New York at Stony Brook, May, 1985.
P. Wolper, “Temporal Logic Can Be More Expressive,” 22nd Annual Symposium on Foundations of Computer Science (1981), pp. 340–347.
A. Yonezawa, “Specification and Verification Techniques for Parallel Programs Based on Message Passing Semantics,” MIT/LCS/TR-191, December, 1977.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stark, E.W. (1986). Proving entailment between conceptual state specifications. In: Robinet, B., Wilhelm, R. (eds) ESOP 86. ESOP 1986. Lecture Notes in Computer Science, vol 213. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16442-1_15
Download citation
DOI: https://doi.org/10.1007/3-540-16442-1_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16442-5
Online ISBN: 978-3-540-39782-3
eBook Packages: Springer Book Archive