| |
 |
|
The metavariables Q,
R, and S range over record types;
P and O range over pointer types;
T and U range over types including
primitives, records, and pointers; V and W range
over all types including primitives, records, pointers, and the
special NILTYPE; f and g
range over field
names; p ranges over method names;
m and n range over method
declaration modifiers; x and y
range over variable names; d and e range over
expressions; le ranges over left expressions; MD
ranges over modules (programs); TD ranges over record
declarations; and PD ranges over method declarations.
Mappings and environments
Like in FMCP, we assume the presence of a fixed Types
table and a fixed Methods table. However, the definitions
and sanity clauses of these tables are somewhat different.
We widen the definition of the type declaration table R
to be a mapping from record or pointer type names R or
P to
type declarations TD. Types(R) denotes
lookup of the type declaration table. As well as the top-level
record type ANYREC (treated as a distinguished record type
name whose definition does not appear in the type declaration
table), we define a pointer type name ANYPTR
such that:
Types(ANYPTR) = POINTER TO ANYREC
In our list of sanity conditions for the type declaration table,
we also add conditions dealing with pointer types. The new type
declaration table sanity conditions are as follows:
- Types(R) = R = ...RECORD... or
Types(P) = R = ...POINTER...
for every R
dom(Types) or
P dom(Types);
- ANYREC
dom(Types);
- For every record type name R or P (except ANYREC) appearing
anywhere in Types, we have R
dom(Types) or P
dom(Types);
- If Types(P) =
POINTER TO R and Types(O) =
POINTER TO R, then P = 0 (i.e. for each
record type, there is an most one corresponding pointer type);
- The subtyping relation <: is antisymmetric (i.e. there are no
cycles in the subtype relation); and
- The inclusion relation
is antisymmetric and antireflexive (i.e.
record types cannot be recursive).
Because the receiver type of methods in IMCP must be a pointer
type, the definition of the method table Methods is
changed accordingly. A method table Methods is now a
mapping from pairs of method names and pointer type names (p, P)
to method declarations PD Methods(p, P)
denotes lookup of the method table. As in FMCP, the method table
maps a pair (p, P) to a method declaration whose receiver
type is exactly P. Methods declared in supertypes of
P are not mapped to P in the method table.
The assumed sanity conditions for the method table are:
- Methods(p, P) =
PROCEDURE (this:P) p ... for every (p, P)
dom(Methods);
- (p, ANYPTR)
dom(Methods); and
- For every type name R or P (except ANYREC) appearing
anywhere in Methods, we have R
dom(Types) or P dom(Types).
|