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=0.7 required=5.0 tests=BAYES_00,MSGID_RANDY
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,cbd507df3efa824b
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2001-02-01 10:20:14 PST
Path: 
 supernews.google.com!sn-xit-02!supernews.com!bignews.mediaways.net!newsfeed.mesh.ad.jp!nntp1.njy.teleglobe.net!teleglobe.net!sunqbc.risq.qc.ca!newsfeed.mathworks.com!news.maxwell.syr.edu!nntp2.deja.com!nnrp1.deja.com!not-for-mail
From: Robert Dewar <robert_dewar@my-deja.com>
Newsgroups: comp.lang.ada
Subject: Re: Help with Atomic_Components and whole array assignment
Date: Thu, 01 Feb 2001 18:10:47 GMT
Organization: Deja.com
Message-ID: <95c8qu$1nb$1@nnrp1.deja.com>
References: <94h55t$9a1$1@nnrp1.deja.com> <94hml1$o64$1@nnrp1.deja.com>
 <94hno6$p8s$1@nnrp1.deja.com> <3A76E455.AABF2490@averstar.com>
 <958o8f$vem$1@nnrp1.deja.com> <3A7886A7.F1BB5513@averstar.com>
 <95bb20$7jb$1@nnrp1.deja.com>
NNTP-Posting-Host: 205.232.38.14
X-Article-Creation-Date: Thu Feb 01 18:10:47 2001 GMT
X-Http-User-Agent: Mozilla/4.61 [en] (OS/2; U)
X-Http-Proxy: 1.0 x70.deja.com:80 (Squid/1.1.22) for client 205.232.38.14
X-MyDeja-Info: XMYDJUIDrobert_dewar
Xref: supernews.google.com comp.lang.ada:4826
Date: 2001-02-01T18:10:47+00:00
List-Id: <comp.lang.ada>

In article <95bb20$7jb$1@nnrp1.deja.com>,
  Rod Chapman <r_c_chapman@my-deja.com> wrote:
> This is what we call the "array update anomaly" in SPARK.
Consider
> the simple assignment statement
>   A(1) := 0;
> This has information flow "derives A from A" since
> 1 element of A is changed and all the others are preserved,
and
> "0" is a literal constant.

This makes perfectly good sense to me, The array update
notation in these kinds of languages is just a short hand
for

   A := A with (1 => 0)

or somesuch, and in that form, it becomes clear that this
derives A from A




>
> The info. flow for a loop is formed (see the maths in Barnes
> or in the Bergeretti/Carre ACM TOPLAS paper) from the
transitive
> closure of the info. flow for its body, so the loop above
does
> indeed have info. flow "derives A from A".
>
> In _general_, the Examiner is not capable of determining that
> all the elements of an array just happen to have been updated
> by a sequence or loop of such statements, and the Examiner
> does not attempt to spot any such special cases.
> (Such as analysis _is_ possible for record fields, though...)
>
> Consider an array A with only 2 elements, and the statements
>   A(I) := 0
>   A(J) := 1;
> where I and J are variables.
>
> Have we updated all the elements of A?  Don't know, so we
have
> to be conservative.  (Flow analysis is essentially syntax
driven -
> we do not attempt to solve proof problems during flow
analysis!)
>
> In real life, if we really need a loop to initialise, then
we'd
> do
>
>   procedure Init ( A : out A_Type );
>   --# derives A from ;
>
>   procedure Init ( A : out A_Type )
>   is
>      --# hide Init;
>   begin
>      ... -- as before...
>   end Init;
>
> instructing the Examiner to believe the spec. and to ignore
the
> body.
>  - Rod
>
> Sent via Deja.com
> http://www.deja.com/
>


Sent via Deja.com
http://www.deja.com/