Next: Contributing, Previous: Dezyne Language Reference, Up: Top [Contents][Index]
The syntax as defined in Dezyne Language Reference leaves room for certain combinations and variations that would lead to Dezyne code that cannot be translated to an mCRL2 process algebra specification. This chapter describes a collection of well-formedness checks that are defined on top of the syntax.
Apart from the syntax checks performed by the parser, five additional categories of checks can be identified:
Upon failure, these produce a undefined identifier
error,
Upon failure, these produce a count mismatch
error,
Upon failure, these produce a type-mismatch
error,
Upon failure, these produce a shadowing
error,
Semantic checks, a.k.a. “well-formedness” checks. Upon failure, these
produce a well-formedness
error.
The first four categories are common programming errors and should not need additional explanation. The last category—the well-formedness checks—are unique to Dezyne and are described in this chapter.
• Well-formedness Checks Categories | Types of checks. | |
• List of Well-formedness Checks | An alphabetical lookup list. | |
• Well-formedness -- Top level | Interfaces, events and components. | |
• Well-formedness -- Directional | Direction of trigger and action. | |
• Well-formedness -- Nesting | The right place for declarative and imperative. | |
• Well-formedness -- Mixing | Mixing of declarative and imperative. | |
• Well-formedness -- Reply | Reply and ports. | |
• Well-formedness -- Valued Actions and Calls | Careful use of values. | |
• Well-formedness -- Injection | Restrictions on injection. | |
• Well-formedness -- Functions | Returning and recursing. | |
• Well-formedness -- Data Parameters | Data type errors. | |
• Well-formedness -- System | Correctly binding all ports. |
Next: Contributing, Previous: Dezyne Language Reference, Up: Top [Contents][Index]