Re: Help with Atomic_Components and whole array assignment

[Robert Dewar <robert_dewar@my-deja.com>]

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/