7.1 Interface Contracts

Dezyne does not have an exception mechanism like other languages. An exception mechanism is designed to prevent accidentally ignoring missed pre- or post-conditions. Instead, in Dezyne the interfaces establish these restrictions by means of verification (See Formal Verification). So where traditional programming languages must handle protocol violations using an exception mechanism at runtime, Dezyne prevents them using the static verification checks⁷. Interfaces in Dezyne are inherently complete with respect to their event alphabet. The generated code will accept every trigger but give an illegal response.

The illegal response is mapped to std::abort () in C++. Note that for a fully verified Dezyne system, operated by clients that adhere to the interface specifications, it is impossible for an illegal response to be triggered. In other words, when an illegal is triggered, it means that some non-Dezyne code is violating a protocol (interface specification).

7.1.1 Implicit interface constraints

Dezyne version 2.17.0 introduces implicit interface constraints.

Before 2.17.0, implementing a component required meticulously specifying the same behavior in the component as in the provides interface; therefore the code from the interface is often repeated in the component.

Since version 2.17.0 the provides interface(s) are implicitly applied as a constraint on the component behavior. This means that anything disallowed by the interface, i.e., explicitly or implicitly marked as illegal, is implicitly marked as illegal in the component behavior.

How does this differ from the existing implicit illegal feature See Illegal you may wonder. The implicit illegal feature leads to implicitly marked illegal behavior when a certain event is ommitted in a certain state. The constraint feature marks as illegal every event in the component behavior which is marked as illegal in the corresponding state in the interface behavior. This avoids the need to repeat the state and guarding from the interface in the component. An example of how this may reduce the behavior specification of a component is the component proxy.