Re: Gnat GPL 2010 available soon (conditional expressions)

[Phil Clayton <phil.clayton@lineone.net>]

On Jun 30, 4:21 am, Britt Snodgrass <britt.snodgr...@gmail.com> wrote:
>
> Yes, and I'll stick with SPARK. I expect future versions of SPARK will
> resist such weirdness.

For formal verification tools, conditional expressions could be
useful.  For example, there are two paths through

  if C then
    Y := A;
  else
    Y := B;
  end if;

but only one path through

  Y := (if C then A else B);

For compliance analysis, the latter could mean only one VC generated
rather than two.  (In an interactive proof of that one VC, yes, you
could end up case splitting on the condition but you're better off
because the case split would only be done if necessary and where
necessary, i.e. possibly just for a part of the overall proof.)

For different types of analysis with SPARK, I'm not sure what the
relative merits would be.

In my view, condition expressions are a step in the right direction...
but I'm the sort of person who wants to write an array aggregate like

  (for I in 1 .. 5 => (for J in 1 .. 7 => (if I = J then 1.0 else
0.0)))

Phil