Ada package specifications: path expressions and monitors

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.