Next: Code Integration, Previous: Formal Verification, Up: Dezyne [Contents][Index]
As Dezyne is intended for operating system like applications, qualifications like trustworthy, secure, safe, robust, and resilient come to mind. Here we discuss how these might be achieved.
If you are dealing with untrustworthy partners, you had better check that they behave as agreed or otherwise stop the transaction. Practically this means that one must not rely blindly on external behavior and external input.
Dezyne interfaces allow you to specify what the implementation can expect from their client and what they must do in return. This is not unlike a contract in terms of a pre-condition and a post-condition. Moreover, verification can be used to exhaustively show that for each Dezyne component these pre- and post-conditions hold. This is what we call See Design by Contract or See Interface Contracts.
Of course any interface contract can be written at the discretion of the designer/programmer. It can either be permissive or restrictive. An astute reader/thinker may realize that pre- and post-conditions are transitive and eventually there will not be a Dezyne implementation behind an interface. This means that verification cannot be used to assert upholding the pre- and post-conditions of the boundary interface. For this boundary we might define a permissive interface (anything goes) to guard the restricted interface and design an adapter component to deal with every request outside of the restricted protocol. This type of component is referred to as an armor (see See Armoring).