From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,334f9012742e58fc
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news2.google.com!postnews.google.com!u7g2000yqm.googlegroups.com!not-for-mail
From: Phil Clayton <phil.clayton@lineone.net>
Newsgroups: comp.lang.ada
Subject: Re: Gnat GPL 2010 available soon (conditional expressions)
Date: Sun, 4 Jul 2010 18:27:04 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: <d66a76c6-5409-409f-85d5-5508aaf9eb41@u7g2000yqm.googlegroups.com>
References: <2010061621145016807-sjs@essexacuk>
 <op.veihbktxnfgb3u@richard.piraten.dd>
	<0fa4c574-9539-492f-8514-d32c68beb22a@w31g2000yqb.googlegroups.com>
	<1frrgtpa5dycl$.12kl72iqsg3dx$.dlg@40tude.net>
 <4c270613$0$6974$9b4e6d93@newsspool4.arcor-online.net>
	<1wuwvzgwlwgli$.1birkinieia0d$.dlg@40tude.net>
 <f1a86f31-598c-4cb1-a60e-011da55f5feb@x27g2000yqb.googlegroups.com>
	<1ur19ais2ejih.mjbgdsv9pr66.dlg@40tude.net>
 <4c275562$0$6987$9b4e6d93@newsspool4.arcor-online.net>
	<4c276114$0$2378$4d3efbfe@news.sover.net> <i0dhh3$qh7$1@munin.nbi.dk>
	<i0e5uc$o4s$1@news.eternal-september.org>
 <7ec98a71-edcb-4851-87fd-6702fb963829@q12g2000yqj.googlegroups.com>
NNTP-Posting-Host: 91.110.215.8
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1278293224 15111 127.0.0.1 (5 Jul 2010 01:27:04
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Mon, 5 Jul 2010 01:27:04 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: u7g2000yqm.googlegroups.com; posting-host=91.110.215.8;
	posting-account=v7gx3AoAAABfjb9m5b7l_Lt2KVEgQBIe
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (X11; U; Linux i686; en-GB; rv:1.9.0.15)
	Gecko/2009102704 Fedora/3.0.15-1.fc10 Firefox/3.0.15,gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:13152
Date: 2010-07-04T18:27:04-07:00
List-Id: <comp.lang.ada>

On Jun 30, 4:21=A0am, 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 :=3D A;
  else
    Y :=3D B;
  end if;

but only one path through

  Y :=3D (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 =3D> (for J in 1 .. 7 =3D> (if I =3D J then 1.0 else
0.0)))

Phil