Re: Help with Atomic_Components and whole array assignment

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

In article <3A76E455.AABF2490@averstar.com>,
  Tucker Taft <stt@averstar.com> wrote:

> I don't agree with Robert on this.  Have you tried writing it
> as a loop rather than an aggregate assignment.

Of course, but that would usually be considered bad style in
SPARK.  The assignment
  A := A_Type'(others => 0);
has information flow "derives A from ;" (i.e. the final value of
A is derived from "nothing" - a constant - which is probably what
you wanted and expected)

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.

Proof of partial correctness is also affected - proving
  --# post A = A_Type'(others => 0);
is trivial in the first case, but rather harder in the latter, so
we nearly always prefer the aggregate.  Our device driver is a fine
example of where we (justifiably) bend the rules... :-)
 - Rod



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