!standard H.8(0)                                09-11-03  AI05-0191-1/01
!class amendment 09-11-03
!status work item 09-11-03
!status received 09-11-03
!priority Low
!difficulty Medium
!subject Aliasing predicates

!summary

** TBD **

!problem

In writing preconditions, one often wants to preclude aliasing situations that
would affect the outcome of a subprogram. Thus, predicates like
    Are_Overlapping(A(I..K), A(J..L))
or  Are_Same(A,B)
would be desirable, where the first asserts that the two arguments overlap in
memory, and the second asserts that the two arguments are in fact occupying the
exact same memory location.

Yet, formulating these predicates in Ada is cumbersome and errorprone.

It would be nice to provide these predicates as part of the language definition.
(Depending on taste, one could instead define Not_Overlapping, Not_Same.)

!proposal

** TBD **

!wording

** TBD **

!discussion

Casting such predicates into the semantic framework of Ada 2005 is surprisingly
difficult.

Since these predicates are defined over the location of the arguments rather
than their values, a definition that employs boolean functions (or attributes)
with these objects as arguments cannot achieve the desired purpose. Passing
parameters by value would have to be prohibited for such functions/attributes,
which would call for language definition magic. In addition, fixing the type of
the parameter(s) introduces restrictions on the generality of the
functions/attributes.

For the same reason, the user cannot define an encapsulating function computing
either predicate for types that allow for passing parameters by value. At best,
he or she can pass addresses and representation lengths to a function that
performs the necessary calculations and comparisons.  This is a rather
unsatisfactory situation, given that these aliasing predicates are conceptually
straightforward.

Given some language magic to solve the parameter passing issue, one then needs
to address the typing of the arguments. Type-safe aliasing can arise for named
entities of the same type or of derivation-related types, where one entity
denotes a view of the other under a different type. The predicate then needs to
accept arguments of equal types or of derivation-related types. Alternatively
one could ask the user for a view conversion to the same type - the solved
parameter passing issue makes sure that the view conversion is not seen as a
value conversion. (It will be seen as a nuisance, though.)

However, this does not cover aliasing achieved by unchecked or unsafe
programming. To extend the predicates to cover this case as well, the predicates
need to accomodate arguments of arbitrary, unrelated types. Again, this cannot
be reasonably done without language magic. (Generics are not a good answer,
since the needed instantiations are gratuitous; they cannot check for anything
and merely add text to the code.)

The simplest language magic would be to introduce a language-defined package
Ada.Predicates, which declares predicates of this general ilk and assigns
semantics to them as desired:

package Ada.Predicates is
   predicate Overlapping (A: <any_type1>; B : <any_type2>);
   predicate Is_Same (A: <any_type1>; B : <any_type2>);
   -- addtional ones surely can be found end Predicates;

The package can gradually be expanded to provide other predicates hard to
program in the language, yet implemented easily by a compiler. I called the
declarations predicates rather than functions to avoid the question of parameter
passing. This is in analogy to the pragma situation. (If you hate the extra key
word, make them boolean functions with Pragma Predicate applying to them. This
pragma alters the parameter semantics and is not available to the user.) The
<any-type> magic needs to be explained and again is not available for the user.

A considerably simpler, but much cruder approach could be the introduction of
language-defined, parameterless predicates
    Aliased_Parameters
    Aliased_Globals
    Aliased_Parameters_or_Globals
defined to be true whenever the named classes of entities in the subprogram
exhibit memory overlaps. Globals refers to any globals named locally in the
subprogram. Usually the last predicate is the most frequently needed one. This
is a special case solution that I do not see as leading towards new and useful
concepts. But a solution it is, partial as it may be.

!example

** TBD **

!ACATS test

An ACATS C test is needed for this feature.

!appendix

****************************************************************