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 checks7. Interfaces in Dezyne are inherently complete with respect to
their event alphabet. The generated code will accept every
trigger but give an
The illegal response is mapped to
std::abort () in
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).
Dezyne version 2.17.0 introduces implicit interface constraints.
Before 2.17.0, for a component to be compliant with its provides interface(s), implementing a component required meticulously specifying the same behavior in the component as in the provides interface(s); therefore the code from the interface(s) 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
How does this differ from the existing implicit illegal feature
illegal you may wonder. The implicit
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.
This is not
unlike languages that use static type analysis and checking (such as
Haskell) versus languages that check types at