## Partial specification annotations

A partial specification annotation can be used to indicate that a CIF specification, such as a library, is meant to be included in other specifications. The annotation is used by the CIF type checker to disable certain types of warnings that may give a lot of false positives for partial specifications. For basic information on partial specification annotations, see the language tutorial. Here we discuss further details.

### Constraints

Partial specification annotations (`@@partial`) can only be added to the specification itself, not to elements of the specification.

The annotation has the following constraints, in addition to the general constraints that apply to all annotations:

- A specification should have at most one partial specification annotation.

- The annotation must not have any arguments.

### Scope

Unlike other annotations, a partial specification annotation applies only to the file in which it is specified. It is not inherited by importing models.

For instance, consider a library model that has a partial specification annotation. The library model is imported into a system model, which does not have a partial specification annotation. The library model has unused events, for which the warnings are suppressed. The system model is not a partial model, and thus the warnings are reported, unless the events are used in the specification model. This prevents false positive warnings in the library model, while warnings about unused events still signal potential modeling issues in the system model.

### Suppressed warnings

The following warnings are suppressed by the CIF type checker for partial specifications:

- Unused events.

- Invariants that restrict events that are not in the synchronization, send or receive alphabet of the specification.