7. Modes and nests

{The identification of a property in a nest is the static counterpart of the dynamic determination {4.8.2.b } of a value in an environ: the search is conducted from the newest (youngest) level towards the previous (older) ones.

Modes are composed from the primitive modes, such as 'boolean', with the aid of 'HEAD's, such as 'structured with', and they may be recursive. Recursive modes spelled in different ways may nevertheless be equivalent. The syntax tests the equivalence of such modes by proving that it is impossible to find any discrepancy between their respective structures or component modes.

A number of unsafe uses of properties are prevented. An identifier or mode-indication is not declared more than once in each reach. The modes of the operands of a formula do not determine more than one operation. Recursions in modes do not cause the creation of dynamic objects of unlimited size and do not allow ambiguous coercions.}

7.1. Independence of properties

{The following syntax determines whether two properties (i.e., two 'PROP's), such as those corresponding to REAL x and INT x, may or may not be enveloped by the same 'LAYER'.}

7.1.1. Syntax

A) PREF :: procedure yielding ; REF to.

B) NONPREF :: PLAIN ; STOWED ; procedure with PARAMETERS yielding MOID ; UNITED ; void.

C) *PREFSETY :: PREF PREFSETY ; EMPTY.

{PROP :: DEC ; LAB ; FIELD.

QUALITY :: MODE ; MOID TALLY ; DYADIC ; label ; MODE field.

TAX :: TAG ; TAB ; TAD ; TAM.

TAO :: TAD ; TAM.}

a) WHETHER PROP1 independent PROPS2 PROP2{a,48a,c ,72a} : WHETHER PROP1 independent PROPS2{a,c} and PROP1 independent PROP2{c}.

b) WHETHER PROP independent EMPTY{48a,c ,72a} : WHETHER true.

c) WHETHER QUALITY1 TAX1 independent QUALITY2 TAX2{a,48a,c ,72a} : unless (TAX1) is (TAX2), WHETHER true ; where (TAX1) is (TAX2) and (TAX1) is (TAO), WHETHER QUALITY1 independent QUALITY2{d}.

d) WHETHER QUALITY1 independent QUALITY2{c} : where QUALITY1 related QUALITY2{e,f,g,h,i,j,-}, WHETHER false ; unless QUALITY1 related QUALITY2{e,f,g,h,i,j,-}, WHETHER true.

e) WHETHER MONO related DUO{d} : WHETHER false.

f) WHETHER DUO related MONO{d} : WHETHER false.

g) WHETHER PRAM related DYADIC{d} : WHETHER false.

h) WHETHER DYADIC related PRAM{d} : WHETHER false.

i) WHETHER procedure with MODE1 parameter MODE2 parameter yielding MOID1 related procedure with MODE3 parameter MODE4 parameter yielding MOID2{d} : WHETHER MODE1 firmly related MODE3{k} and MODE2 firmly related MODE4{k}.

j) WHETHER procedure with MODE1 parameter yielding MOID1 related procedure with MODE2 parameter yielding MOID2{d} : WHETHER MODE1 firmly related MODE2{k}.

k) WHETHER MOID1 firmly related MOID2{i,j} : WHETHER MOODS1 is firm MOID2{l,m} or MOODS2 is firm MOID1{l,m}, where (MOODS1) is (MOID1) or (union of MOODS1 mode) is (MOID1), where (MOODS2) is (MOID2) or (union of MOODS2 mode) is (MOID2).

l) WHETHER MOODS MOOD is firm MOID{k,l} : WHETHER MOODS is firm MOID{l,m} or MOOD is firm MOID{m}.

m) WHETHER MOID1 is firm MOID2{k,l,n,47f } : WHETHER MOID1 equivalent MOID2{73a } or MOID1 unites to MOID2{64b } or MOID1 deprefs to firm MOID2{n}.

n) WHETHER MOID1 deprefs to firm MOID2{m} : where (MOID1) is (PREF MOID3), WHETHER MOID5 is firm MOID2{m}, where MOID3 deflexes to MOID5{47a,b,c } ; where (MOID1) is (NONPREF), WHETHER false. {To prevent the ambiguous application of indicators, as in REAL x, INT x; x:=0, certain restrictions are imposed on defining-indicators contained in a given reach. These are enforced by the syntactic test for "independence" of properties enveloped by a given 'LAYER' (rules a, b, c). A sufficient condition, not satisfied in the example above, for the independence of a pair of properties, each being some 'QUALITY TAX', is that the 'TAX's differ (rule c). For 'TAX's which are not some 'TAO', this condition is also necessary, so that even REAL x, INT x; SKIP is not a serial-clause.

For two properties 'QUALITY1 TAO' and 'QUALITY2 TAO' the test for independence is more complicated, as is exemplified by the serial-clause

OP + = (INT i)BOOL: TRUE, OP + = (INT i , j)INT: 1, OP + = (INT i, BOOL j)INT: 2, PRIO + = 6; 0 + + 0 ¢ = 2 ¢. Ambiguities would be present in

PRIO + = 6, + = 7; 1 + 2 * 3 ¢ 7 or 9 ? ¢ , in

OP Z = (INT i)INT: 1, MODE Z = INT; Z i ¢ formula or declaration? # ; SKIP, and in

OP ? = (UNION(REF REAL, CHAR) a)INT: 1, OP ? = (REAL a)INT: 2; ?LOC REAL ¢ 1 or 2 ? ¢.

In such cases a test is made that the two 'QUALITY's are independent (rules c, d). A 'MOID TALLY' is never independent of any 'QUALITY' (rule d). A 'MONO' is always independent of a 'DUO' (rules d, e, f) and both are independent of a 'DYADIC' (i.e., of a 'priority PRIO') (rules d, g, h). In the case of two 'PRAM's which are both 'MONO' or both 'DUO', ambiguities could arise if the corresponding parameter modes were "firmly related", i.e., if some (pair of) operand mode(s) could be firmly coerced to the (pair of) parameter mode(s) of either 'PRAM' (rules i, j). In the example with the two definitions of ?, the two 'PRAM's are related since the modes specified by UNION (REF REAL, CHAR) and by REAL are firmly related, the mode specified by REF REAL being firmly coercible to either one.

It may be shown that two modes are firmly related if one of them, or some component 'MOOD' of one of them, may be firmly coerced to the other (rules k, l), which requires a sequence of zero or more meek coercions followed by at most one uniting {6.4.1.a }. The possibility or otherwise of such a sequence of coercions between two modes is determined by the predicate 'is firm' (rules m, n).

A 'PROP1' also renders inaccessible a 'PROP2' in an outer 'LAYER' if that 'PROP2' is not independent of 'PROP1'; e.g.,.

BEGIN INT x;
BEGIN REAL x; ¢ here the 'PROP1' is 'reference to real letter x' ¢
SKIP
END
END

and likewise

BEGIN OP ? = (INT i)INT: l, INT k:=2;
BEGIN OP ? = (REF INT i)INT: 3;
    ? k ¢ delivers 3, but ? 4 could not occur here because its operator is inaccessible ¢
END

. }

Next