Re: When to do a constraint check and not ??

[Peter Amey <peter.amey@praxis-cs.co.uk>]

Per Sandberg wrote:
> 
> Assume the folowing code:
> 
> procedue bla is
>         b : boolean; --< B may contain any bit pattern at this point.
> 
>         procedure test( p : in out boolean ) is
>         begin
>                 b := false;
>         end test;
> 
> begin
>         test(b); --<< Is the compiler allowed to insert a constraint check on b
> here ??
> end;
> 

FWIW, SPARK has an interesting take on this kind of problem.  Firstly,
SPARK annotations identify whether data is being imported to and/or
exported from a procedure; this must be consistent with parameter
modes.  So, based on its parameter mode in the above example, p of
procedure test would have to be both an import and an export.  This has
two consequences: (1) flow analysis will show that it isn't true (since
p is actually a pure export of test) and (2) a data flow error
(reference to uninitialized variable) will be raised at the call "test
(b)". 

If the correct annotation ("derives p from ;") is placed on test then
the rules of SPARK require the parameter mode to be made "out" and the
potential data flow error is removed.

Finally, SPARK protects from another problem in the example.  I assume
that the body of test is supposed to have the assignment "p := false"
rather than "b := false".  In Ada "b" is of course visible at this point
so the incorrect assignment is legal.  In SPARK, b is not visible unless
it is placed in a global annotation on test.  In this way we prevent
accidental holes in scope.

I know that this does not really answer the original question but I
couldn't help observing how often the difficult questions people raise
about odd corners of the Ada language turn out not to be issues at all
for SPARK.

regards



Peter

---------------------------------------------------------------------------   
      __         Peter Amey, Product Manager
        )                    Praxis Critical Systems Ltd
       /                     20, Manvers Street, Bath, BA1 1PX
      / 0        Tel: +44 (0)1225 466991
     (_/         Fax: +44 (0)1225 469006
                 http://www.praxis-cs.co.uk/

--------------------------------------------------------------------------