Re: Help with Atomic_Components and whole array assignment

[Rod Chapman <r_c_chapman@my-deja.com>]

In article <3A7886A7.F1BB5513@averstar.com>,
  Tucker Taft <stt@averstar.com> wrote:
> Rod Chapman wrote:
> > The compound statement
> >    for I in A'Range loop
> >       A(I) := 0;
> >    end loop;
> > has information flow "derives A from A", which is significantly
> > different.
>
> I don't understand why this derives A from A.  Is this just
> a limitation of SPARK?  Clearly, we are assigning a new
> value to every component of A, making no use of the original
> values.

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.

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/