© 1986 by British Computer Society
A Proof System for Ada* Tasks


Department of Computer Science, University of Manchester, Oxford Road, Manchester M13 9PL, UK
An axiomatic proof system for reasoning about the basic Ada tasking constructs is presented. The proof system is based on an earlier paper by the same authors and deals with safety properties of concurrent Ada programs including freedom from deadlock. The system has been proved to be sound and relatively complete against a denotational semantics for the constructs considered.
Received March 1985.
* Ada is a registered trademark of the U.S. Government (Ada Joint Program Office).
Department of Computer Science, University of Manchester, Oxford Road, Manchester M13 9PL
¶ Present address: Data Systems Division, Marconi Radar Systems Ltd, Writtle Road, Chelmsford CM1 3BN, England.