7.4. Well-formedness {A mode is well formed if
7.4.1. Syntax a) WHETHER (NOTION) shields SAFE to SAFE{73c } : where (NOTION) is (PLAIN) or (NOTION) is (FLEXETY ROWS of) or (NOTION) is (union of) or (NOTION) is (void), WHETHER true.
b) WHETHER (PREF) shields SAFE to yin SAFE{73c } : WHETHER true.
c) WHETHER (structured with) shields SAFE to yang SAFE{73c } : WHETHER true.
d) WHETHER (procedure with) shields SAFE to yin yang SAFE{73c } : WHETHER true. {As a by-product of mode equivalencing, modes are tested for well-formedness {7.3.1.c }. All nonrecursive modes are well formed. For recursive modes, it is necessary that each cycle in each spelling of that mode (from 'MU definition of MODE' to 'MU application') passes through at least one 'HEAD' which is yin, ensuring condition (i) and one (possibly the same) 'HEAD' which is yang, ensuring condition (ii). Yin 'HEAD's are 'PREF' and 'procedure with'. Yang 'HEAD's are 'structured with' and 'procedure with'. The other 'HEAD's, including 'FLEXETY ROWS of' and 'union of', are neither yin nor yang. This means that the modes specified by A, B and C in
MODE A = STRUCT(INT n, REF A next), B = STRUCT(PROC B next), C = PROC(C)C