Axioms and proof rules for Ada tasks
- 1 January 1982
- journal article
- Published by Institution of Engineering and Technology (IET) in IEE Proceedings E Computers and Digital Techniques
- Vol. 129 (2) , 38-48
- https://doi.org/10.1049/ip-e.1982.0010
Abstract
An axiomatic proof system is developed for use in proving partial correctness and absence of deadlock in Ada tasks. Axioms for the Ada tasking primitives in isolation are presented, and then rules proposed that describe the logical interaction of tasks through the rendezvous mechanism. These axioms and rules are then used to present partial correctness proofs of parallel-processing examples written in Ada. The system is extended to deal with questions of blocking and detection of deadlock and, finally, the problems of task termination and exception handling are discussed.Keywords
This publication has 2 references indexed in Scilit:
- On the absence of livelocks in parallel programsPublished by Springer Nature ,2005
- Cooperating Sequential ProcessesPublished by Springer Nature ,1968