Re: SPARK flow analysis (was Help with Atomic_Components and whole array assignment)

[Stuart Palin <stuart.palin@baesystems.com>]

Tucker Taft wrote:
<with snipping; use snipping;>

> Rod Chapman wrote:
> > 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.
> 
> 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.

You are correct in that in the overall scheme of things A does not
derive from A, because in both cases A is entirely defined as 0. 
However, in the first case the fact that A is fully defined as 0 is
obvious from the _syntax_ of the single statement; whereas in the second
case it only becomes apparent from the _semantics_ of the set of
statements.

The SPARK Examiner analyses code at 2 levels; the less sophisticated of
the two is Flow Analysis which reports on the apparent behaviour of a
subprogram based upon the cumulative effects of statements, using only
the simple syntactic properties of each statement.  Despite being a
"simpler" analysis it is still quite capable of detecting significant
classes of faults, and the more the code behaviour is reflected in the
syntax the better the analysis.
(The value of flow analysis is that it can help eliminate many common
programming errors before investing time and effort into creating proofs
of correctness - or rather, if the program is flawed, failing to produce
a proof and realising your mistake after many hours).

Another example of syntax v semantics would be:
      if B then                if B then
         x := 0;                  x := 0;
      else                     end if;
         x := 1;
      end if;                  if not B then
                                  x := 1;
                               end if;


In the left hand case the fact that x is only dependent on B is clear
from the syntax; whereas in the right hand case this only becomes clear
from the semantics (Flow analysis of the right hand case would suggest
that x may depend on its original value as well as B.  This is because
until you examine the semantics and establish that if x has not been
assigned the value 0 it must be assigned 1.  Looking at the syntax alone
suggests that there might be a path through the code in which x is never
given a value (it also suggests there might be a path in which it is
assigned the value 0 then, without that being used, it might be
re-assigned the value 1: but that is a different story and a different
warning).

When you use SPARK to do semantic analysis and construct program proofs
you would would be able to show that the two programs are equivalent.

--
Stuart Palin
Principal Software Engineer
BAE SYSTEMS Avionics Ltd, Rochester