Abstract
A rudimentary exit-mechanism from the parallel command of the language fragment CSP is introduced. A method for embedding invariants in a standard partial correctness system with pre-and postconditions is presented. Proof rules for exits from concurrent systems are introduced, and a simple data flow system is verified.
Similar content being viewed by others
References
C. A. R. Hoare,Communicating sequential processes. Communications of the ACM, 21(8): 666–677, 1978.
Reference Manual for the Ada Programming Language. U.S. Department of Defense, January 1983. ANSI/MIL-STD-1815A.
Occam Programming Manual. INMOS, 1983.
Sigurd Meldal,An axiomatic semantics for nested concurrency. BIT 26: 2, 164–174, 1986.
Sigurd Meldal,Predicting the future: Proof-rules for exceptions in concurrent structures. Research Report 101, Institute of Informatics, University of Oslo, April 1986.
Sigurd Meldal,Language elements for hierarchical abstraction in concurrent structures. Research Report 102, Institute of Informatics, University of Oslo, March 1986.
Neelam Soundararajan and Ole-Johan Dahl,Partial correctness semantics of CSP. Research Report 66, Institute of Informatics, University of Oslo, February 1982.
Stephen A. Cook,Soundness and completeness of an axiom system for program verification. SIAM Journal on Computing, 7(1): 70–90, February 1978.
David C. Luckham and Wolfgang Polak,Ada exception handling — An axiomatic approach. ACM Transactions on Programming Languages and Systems, 2, 1980.
Ole-Johan Dahl,Can program proving be made practical? In M. Amirchahy and D. Neel, editors,Les Fondements de la Programmation, pages 56–115, CCE-CREST, IRIA, December 1977. Also in: Research report no. 33, Institute of Informatics, University of Oslo.
Krzysztof R. Apt,Ten years of Hoare's logic: A survey — Part 1. ACM Transactions on Programming Languages and Systems, 3(4): 431–483, 1981.
Sigurd Meldal,Axiomatic semantics for access type tasks in Ada. Research Report 100, Institute of Informatics, University of Oslo, April 1986. Invited paper at the meeting of Ada Europe — Working Group on Formal Methods, February 6th 1986.