Information Technology Reference
In-Depth Information
M }
.
,where
¯
¯
as follows:
class
C
extends
D {
T
f
stands for typed fields in the
¯
f
;
¯
¯
T
¯
class, while
M
represents a list of methods.
Only
bool
and
unit
(the empty type) are predefined as primitive types in the
language; from these types, other primitives may be built. Furthermore, expres-
sions do not have side effects; object construction occurs only as a command.
Similarly, method calls occur in special assignments
x:= e.m(
e
)
defining both
side effect and a return value. Methods can be defined recursively, so loops are
omitted.
We adapted to this language a complete set of laws of programming [18]. The
following law, for instance, establishes that instantiations of a class
B
can be
replaced by instantiations of its superclass
A
,aslongas
B
is an empty class. This
replacement can occur either in the body of
A
's methods or any method in the
set of class declarations
CT
(a class table).
CT
[
exp
/exp
] denotes a substitution.
Replacement is applicable when expressions of type
A
are not cast with
B
and
B
instances are assigned only to
A
-typed variables. The opposite application is
constrained by a proviso: tests involving
A
-typed variables with
B
may not work
if
A
's instances become
B
instances.
fds
and
mts
represent, respectively, fields
and methods. A primed metavariable, like
mts
, is a transformed version of the
unprimed one, as defined in the
where
clause. A sample of other laws used in
this paper are presented in a technical report [22].
Law 1
new superclass
class
A
extends
C {
fds
mts
class
B
extends
A {}
CT
class
A
extends
C {
fds
mts
class
B
extends
A {}
CT
=
where
CT
=
CT
[
new
A/
new
B
]
mts
=
mts
[
new
A/
new
B
]
provided
(
→
)(1)
B
is not used in type casts or tests in
CT
or
mts
for expressions of type
A
;
(2)
x
:=
new
B
only appears if
type
(
x
)
≤ A
;
(
←
) Variables of type
T ≤ A
are not involved in tests with type
B
.
In addition to equivalence laws, there are laws for
class refinement
that involve
internal representation changes such as addition and removal of private fields.
In these laws, simulation is established within a class by a constructor making
the coupling invariant true and every method executing on a valid state and
resulting in another valid state, as they are based on Morgan's refinement no-
tion [23]. These laws have been proven sound and complete as well, although
within a language lacking object references [18]. In order to avoid this limitation
in work, we guarantee modular reasoning by using
confinement
as a requirement
for programs.
Ownership confinement
[24] is a discipline for controlling aliasing in object-
oriented languages, restricting access to designated
representation objects
(reps),
except through their
owners
, to avoid representation exposure [19]. An owner
is a class that maintains representation objects stored in the fields of its
Search WWH ::
Custom Search