Re: Gnat GPL 2010 available soon (conditional expressions)

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

On Jul 5, 11:26 am, Georg Bauhaus <rm.dash-bauh...@futureapps.de>
wrote:
> On 05.07.10 03:27, Phil Clayton wrote:
>
> > On Jun 30, 4:21 am, Britt Snodgrass <britt.snodgr...@gmail.com> wrote:
> > 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);
>
> Any advantage over a function---which in SPARK case will
> be a pure function, IIRC?
>
>   Y := Find_Y (Depends => C);

Not much advantage over a function, only that you don't have the
overheads of introducing the new function and ensuring its
specification has sufficient information.  I wasn't really considering
the possibility of introducing new functions as a general
alternative.  For example, I would rather see certain conditional
expressions inline and not tucked away inside functions, for
readability.

(Correct, SPARK does not allow functions to have side effects.)


> > 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)))
>
> What kind of name would you pick for the thing?

I suppose I'd call it a 'tabulation'..

Phil