Information Technology Reference
In-Depth Information
Let us consider again the refinement mapping presented in Figure 3. In this case, the
set
V
is the singleton set
and only the satisfaction of condition 8 requires some
reasoning. According to the definition of the class
MyListWMerge
, type variable
E
must extend
Mergeable<E>
, which, in turn, declares method
E merge(E e)
. Hence,
the instantiation of
E
is limited to classes
C
that implement
Mergeable<C>
and, hence,
it is ensured that
C
possesses a method with signature
C merge(C e)
.
In the sequel, we assume a fixed refinement mapping
{
E
}
R
between a specification
module
M
and a Java program
J
. Intuitively,
J
is in conformity with
M
iff:
and
(ii) the algebraic properties of the notion of equality
hold in every possible execution of the program
(i) the properties specified in
M
.
More concretely, the properties of a core specification
S
impose constraints on the be-
havior of every object of type
T
S
=
R
(
J
, whereas the properties of a parameter spec-
ification
S
used in a parameterized specification, say
S
[
S
)
S
]
, impose constraints on the
behavior of every object of a type
T
S
in
J
that is used to instantiate the respective type
S
)
variable of the generic type
R
(
. Axioms and domain conditions impose different
type of constraints:
Axioms.
Every axiom in a specification
S
defines, for the objects of type
T
S
, a property
that must hold in all client visible-states.
Let us consider, for instance, the first axiom for
get
in
ListWM[Mergeable]
.Let
lwm
be an object of type
MyListWMerge<C>
. This axiom defines that for every
non-null expression
e
of type
C
, after the execution of
lwm.addFirst(e)
,the
expression
lwm.get(0).equals(e)
evaluates to true
1
.
Domains.
Every domain condition
φ
of an operation
op
of a specification
S
defines
that, for every object of type
T
S
, whenever
φ
holds, the invocation of
R
(
op
)
must
return normally (i.e., does not throw an exception).
The constraints induced by axioms and domain conditions just presented define a notion
of conformance. C
ON
G
U
, by default, uses a stronger notion that, in addition, also im-
poses restrictions on the clients of the classes
T
S
, namely when they invoke a method
R
(
: it is required that the
null
value is not passed as argument and the domain
condition
φ
holds at the time the method
op
)
is invoked.
This stronger notion of conformance is useful for checking that client code does not
call methods in situations where it is not possible assess the normal (non-exceptional)
return of a method called outside its domain condition. This is however only appro-
priate in the absence of additional information about the safe calling conditions for
such methods. For instance, if the documentation of class
MyListWMerge<E>
says that
void
set(E e,
int
i)
has no pre-condition and simply produces no effect on the
state of the list when
i>size()
, the fact that a class in our program calls this method
with an argument that violates this condition should not be identified as a problem of
conformance between the program and the specification module
LWM
. For this reason,
we found useful to support the two notions of conformance in C
ON
G
U
2.
R
(
op
)
1
We currently assume that the interpretation of sorts does not include the
null
value but, we
envisage that, in the future, refinement mappings may define whether this is appropriate or not.
Search WWH ::
Custom Search