We would like to add as a last note concerning assertion checking,
that some assertions which are not checkable in the general case, can
sometimes be proven statically safe because of the context, due to a
phenomenon which we could call assertion inference. A simple example
will again tell more than a long explanation.
A typical stack has two members, "push" and "pop", which have
respectively as post- and pre- condition the assertion "stack non
empty". Although in general it can only be checked dynamically,
everybody must admit that (barred stack overflow), the following
sequence of instructions is statically safe:
stack.push(item);
stack.pop();
We don't know of any compiler or language which would exploit
considerations of this kind. Similar situations can apply when dealing
with covariance, e.g. in the somehow simpler case of dual hierarchies.
We will reuse our zoo example to make our point.
Animals eat food, but giraffes eat leaves, while lions eat meat.
Let's have a dual hierarchy of guards, who provide food to animals. We
have thus specialized giraffe_guards and lion_guards, who provide the
appropriate kind of food for the respective kind of animal. Let's
further suppose that every animal has its own guard, of a trustable
kind. Now the function:
void foo(Animal& a) {
a.eat(a.guard().provide_food());
}
is statically safe although we know neither the actual kind of
food which is provided and eaten nor the specialty of the guard taking
care of the animal "a", because of some kind of context dependent
assertion inference.
Using techniques such as the ones presented in (b), which ally
behaviour specification and dedicated interfaces, one can take
advantage of this static safety unsupported by the language, to
justify, in a controlled, dedicated scope, a dynamic cast.
If the "eat" member can be guaranteed to be accessed only from
within scopes such as the above function foo, it may safely, in each
specialized animal type, cast its input parameter from the type
"food", into the appropriate type of food for it to be processed
according to its specificity.