摘要:

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.

DOI:10.1049/ip-e.1982.0010

出版商:IEE    

年代:1982

数据来源: IET

摘要:

The paper describes how path expressions can be introduced in an Ada package specification to define the permitted interleavings between calls on the functions and procedures in the visible part of the package. A preprocessor is described which synthesises the internal task and entry calls required to enforce the specified protocols.

DOI:10.1049/ip-e.1982.0011

出版商:IEE    

年代:1982

数据来源: IET

摘要:

One of the design aims of Ada was to provide a language which would encourage the production of reliable programs: An important technique used to provide greater reliability is program verification. In this paper, we comment on the design of Ada from this particular point of view and we indicate particular approaches to the verification of Ada programs.

DOI:10.1049/ip-e.1982.0012

出版商:IEE    

年代:1982

数据来源: IET

摘要:

This paper describes the structure and tasking features of the programming language Martlet. Martlet is based on two languages: Pascal and the US Department of Defence language Ada. Essentially, the sequential part of the language is Pascal and this has been extended to include a number of the structural and tasking features of Ada. The latter are described in the paper, and also the overheads required to implement these features on an actual multiprocessor structure are presented.

DOI:10.1049/ip-e.1982.0013

出版商:IEE    

年代:1982

数据来源: IET

摘要:

An outline of a formalism for writing specifications of synchronisation behaviours is given, together with a sketch of an approach to the transformation between such a specification and an implementation in Ada. The model of implementation is that each specification is regarded as defining a mechanism, the 'object manager', which controls the occurrence of events in the system. Each object manager is implemented as an Ada package that provides a collection of procedures to a collection of tasks. Hidden inside the package are 'shared' data structures and a synchronisation task which schedules the start of execution of each procedure call.

DOI:10.1049/ip-e.1982.0014

出版商:IEE    

年代:1982

数据来源: IET

摘要:

The design of the Ada arithmetic capabilities is presented as an elaborate compromise between conflicting requirements of efficiency and machine independence. The costs and benefits incurred by this compromise are explored in some detail and some areas for eventual investigation in the light of future experience with Ada arithmetic are identified.

DOI:10.1049/ip-e.1982.0015

出版商:IEE    

年代:1982

数据来源: IET