From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,139d9b90ab37c0e5
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2001-11-05 02:02:12 PST
Path: 
 archiver1.google.com!news1.google.com!sn-xit-02!supernews.com!news.tele.dk!small.news.tele.dk!130.133.1.3!fu-berlin.de!uni-berlin.de!213.155.153.242!not-for-mail
From: Peter Amey <peter.amey@praxis-cs.co.uk>
Newsgroups: comp.lang.ada
Subject: Re: When to do a constraint check and not ??
Date: Mon, 05 Nov 2001 10:02:45 +0000
Organization: Praxis Critical Systems
Message-ID: <3BE663C5.78C8EBF2@praxis-cs.co.uk>
References: <3BD91EF8.EEB7EDBA@systems.saab.se>
NNTP-Posting-Host: 213.155.153.242
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
X-Trace: fu-berlin.de 1004954530 34454155 213.155.153.242 (16 [69815])
X-Mailer: Mozilla 4.73 [en] (Windows NT 5.0; U)
X-Accept-Language: en
Xref: archiver1.google.com comp.lang.ada:15795
Date: 2001-11-05T10:02:45+00:00
List-Id: <comp.lang.ada>



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/

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