Leslie Lamport
ABSTRACT
The formal correspondence between an implementation and its specification is examined. It is shown that existing specifications that claim to describe priority are either vacuous or else too restrictive to be implemented in some reasonable situations. This is illustrated with a precisely formulated problem of specifying a first-come-first-served mutual exclusion algorithm, which it is claimed cannot be solved by existing methods.
- {1} John Bethel, ed. Webster's New Collegiate Dictionary. G. & C. Meriam Co., Springfield, Mass. (1956).Google Scholar
- {2} P. J. Courtois, F. Heymans and D. L. Parnas. Concurrent Control with "Readers" and "Writers". Comm. ACM 14, 10 (October 1971), 667-668. Google ScholarDigital Library
- {3} E. W. Dijkstra. Solution of a Problem in Concurrent Programming Control. Comm. ACM 17, 11 (November 1974), 643-644. Google ScholarDigital Library
- {4} Susan Gerhart et al. An Overview of AFFIRM: A Specification and Verification System, IFIP Congress 80, (Oct. 1980).Google Scholar
- {5} Irene Greif. A Language for Formal Problem Specification, Comm. ACM 20, 12 (Dec. 1977), 931-935. Google ScholarDigital Library
- {6} J. V. Guttag and J. J. Horning. Formal Specification as a Design Tool. Proc. ACM Symposium on Principles of Programming Languages, Las Vegas, (January 1980), 251-261. Google ScholarDigital Library
- {7} J. V. Guttag and J. J. Horning. An Introduction to the Larch Shared Language. Proc. IFIP Congress '83, Paris, (1983).Google Scholar
- {8} Brent Hailpern. Verifying Concurrent Processes Using Temporal Logic, Lecture Notes in Computer Science 129, Springer-Verlag (1982). Google ScholarDigital Library
- {9} Howard Katseff. A Solution to the Critical Section Problem with a Totally Wait-free FIFO Doorway. Technical Memorandum, Computer Science Division, University of California, Berkeley.Google Scholar
- {10} Leslie Lamport. A New Solution of Dijkstra's Concurrent Programming Problem, Comm. ACM 17, 8 (Aug. 1974), 453-455. Google ScholarDigital Library
- {11} Leslie Lamport. Specifying Concurrent Program Modules, ACM Trans. on Prog. Lang. and Systems 5, 2 (Apr. 1983), 190-222. Google ScholarDigital Library
- {12} Leslie Lamport. What Good is Temporal Logic? Information Processing 83, R. E. Mason (ed.), Elsevier Science Publishers (North-Holland), 1983, 657-668.Google Scholar
- {13} Amy Lansky and Susan S. Owicki. GEM: A Tool for Concurrency Specification and Verification, Proc. of the Second Annual ACM Symposium on Principles of Dietributed Computing (Aug. 1983), 198-212. Google ScholarDigital Library
- {14} Peter E. Lauer, P. Torrigiani and M. Shields. COSY: A System Specification Language Based on Paths and Processes, Acta Informatica 12 (1979), 109-158.Google ScholarDigital Library
- {15} Robin Milner. A Calculus of Communicating Systems , Lecture Notes in Computer Science 92, Springer-Verlag (1980). Google ScholarDigital Library
- {16} Richard L. Schwartz and P. M. Melliar-Smith. Temporal Logic Specification of Distributed Systems, Proc. of the IEEE Conjerence on Distributed Systems, (Apr. 1979).Google Scholar
- {17} Richard L. Schwartz, P. M. Melliar-Smith and F. H. Vogt. An Interval Logic for Higher-Level Temporal Reasoning, Proc. of the Second Annual ACM Symposium on Principles of Distributed Computing (Aug. 1983), 198-212. Google ScholarDigital Library
- {18} Pierre Wolper. Specification and Synthesis of Communicating Processes Using an Extended Temporal Logic, Proc. of the Conference on the Principles of Programming Languages, Albuquerque (Jan. 1982). Google ScholarDigital Library
Index Terms
- What it means for a concurrent program to satisfy a specification: why no one has specified priority
Recommendations
Specification, Refinement and Verification of Concurrent Systems—An Integration of Object-Z and CSP
This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of ...
The state-based CCS semantics for concurrent Z specification
ICFEM '97: Proceedings of the 1st International Conference on Formal Engineering MethodsPresents a formal method which combines the Z notation and value-passing CCS (Calculus of Communicating Systems) for specifying concurrent systems. In order to provide a sound theoretical basis for the method, the state-based semantics for value-passing ...
Comments