---

11 Well-formedness

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:

definition checks

Upon failure, these produce a undefined identifier error,

parameter checks

Upon failure, these produce a count mismatch error,

type checks

Upon failure, these produce a type-mismatch error,

shadowing checks

Upon failure, these produce a shadowing error,

well-formedness checks

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
• List of Well-formedness Checks
• Well-formedness – Top level
• Well-formedness – Directional
• Well-formedness – Nesting
• Well-formedness – Mixing
• Well-formedness – Reply
• Well-formedness – Valued Actions and Calls
• Well-formedness – Injection
• Well-formedness – Functions
• Well-formedness – Data Parameters
• Well-formedness – System