×

zbMATH — the first resource for mathematics

Partial correctness of exits from concurrent structures. (English) Zbl 0599.68029
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.

MSC:
68N25 Theory of operating systems
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
Ada95
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] C. A. R. Hoare,Communicating sequential processes. Communications of the ACM, 21(8): 666–677, 1978. · Zbl 0383.68028 · doi:10.1145/359576.359585
[2] Reference Manual for the Ada Programming Language. U.S. Department of Defense, January 1983. ANSI/MIL-STD-1815A.
[3] Occam Programming Manual. INMOS, 1983.
[4] Sigurd Meldal,An axiomatic semantics for nested concurrency. BIT 26: 2, 164–174, 1986. · Zbl 0594.68026 · doi:10.1007/BF01933742
[5] Sigurd Meldal,Predicting the future: Proof-rules for exceptions in concurrent structures. Research Report 101, Institute of Informatics, University of Oslo, April 1986. · Zbl 0599.68029
[6] Sigurd Meldal,Language elements for hierarchical abstraction in concurrent structures. Research Report 102, Institute of Informatics, University of Oslo, March 1986. · Zbl 0599.68029
[7] Neelam Soundararajan and Ole-Johan Dahl,Partial correctness semantics of CSP. Research Report 66, Institute of Informatics, University of Oslo, February 1982.
[8] Stephen A. Cook,Soundness and completeness of an axiom system for program verification. SIAM Journal on Computing, 7(1): 70–90, February 1978. · Zbl 0374.68009 · doi:10.1137/0207005
[9] David C. Luckham and Wolfgang Polak,Ada exception handling – An axiomatic approach. ACM Transactions on Programming Languages and Systems, 2, 1980. · Zbl 0468.68014
[10] 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.
[11] 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. · Zbl 0471.68006 · doi:10.1145/357146.357150
[12] 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. · Zbl 0594.68026
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.