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,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: 103376,af40877501f46910,start
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,UTF8
Path: 
 g2news1.google.com!news3.google.com!feeder.news-service.com!news.mixmin.net!aioe.org!not-for-mail
From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?=
 =?utf-8?Q?=29?=
 <yannick_duchene@yahoo.fr>
Newsgroups: comp.lang.ada
Subject: SPARK understand me very well... me neither
Date: Fri, 13 Aug 2010 22:12:54 +0200
Organization: Ada At Home
Message-ID: <op.vhd7rsl2ule2fv@garhos>
NNTP-Posting-Host: M2yP1Cx/h9YxW/Ct5b534Q.user.speranza.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes
Content-Transfer-Encoding: Quoted-Printable
X-Complaints-To: abuse@aioe.org
X-Notice: Filtered by postfilter v. 0.8.2
User-Agent: Opera Mail/10.60 (Win32)
Xref: g2news1.google.com comp.lang.ada:13241
Date: 2010-08-13T22:12:54+02:00
List-Id: <comp.lang.ada>

Hello,

I've opened a thread about it some months ago. Here is a new opportunity=
  =

to come back to this topic : help you (and me) and SPARK to better  =

understand each others. I am not talking about the language, ... about t=
he  =

simplifier (and may a bit about the examiner which do a bit a the  =

simplifier's job).

User rules kept apart because this may be better to avoid it as much as =
 =

possible I feel, and because sometime this may be advised to strictly  =

avoid it (see below), guessing what the simplifier will be able to to wi=
th  =

this and that is a cool affair. There is a kind of feeling involved here=
,  =

and it is less predictable than the grammatical validity of a given  =

compilation unit.

This is always what I am facing. I had previous experiences which shown =
 =

using a lot of --# check to attempt to build a step by step proof can en=
d  =

into a very long Simplifier execution time (I have meet a case where it =
 =

was needed as much as 20 minutes on a simple procedure... due to the  =

assert clauses I used). Although this may work nice, this technique has =
 =

some limits. This is at least what I have learned since my previous  =

experiences.

I have posted a second example for SPARK at Rosetta today,  =

http://rosettacode.org/wiki/Function_definition#SPARK , which uses an  =

if-then-elsif block. This works nice, validate nice, no trouble with thi=
s  =

one (just notice I needed two separate branches, one for A =3D 0 and ano=
ther  =

for B =3D 0, because a single one for =E2=80=9C(A =3D 0) or (B =3D 0)=E2=
=80=9D was not provable  =

at all by the Simplifier).

I wanted to make this more light and simple, dropping this if-then-elsif=
  =

block. Doing so, I am facing some incomprehension between me and SPARK  =

(but as it is one of my friend, I feel it is worth the effort to still g=
o  =

on with it).

I came to two points : the first one, I've already meet it in the past, =
 =

but never talked about it ; the second one, is hard to me, as I don't wa=
nt  =

to rely on any user rule for examples posted at Rosetta.

The first one is that if I want to get ride of these if-then-elsif  =

branches, I do not know another way except using P1 -> Pn where P1 stand=
s  =

for the same expressions as the ones which was in if-elsif condition  =

expressions. OK, this looks fine, except if I want to move multiple Chec=
k  =

or Assert outside of conditional branch, as I have to prefix all of thes=
e  =

with the "P1 -> " and if P1 is a quite complex expression, this can lead=
  =

to unreadable things (I am not just talking about the example at Rosetta=
  =

here).

I was wondering if it is good or bad practice to use language construct =
to  =

makes things provable instead of using Check and Assert. It seems to me,=
  =

language constructs may be more efficient is some cases, but I still wou=
ld  =

like to read opinions about it.

The second one, is one of this so simple things I am failing to express =
:  =

I can get (A =3D 0) or not (A =3D 0) to validate successfully, but I can=
't get  =

(A =3D 0) or (A /=3D 0) to validate as much successfully (fails), while =
it can  =

prove (not (A =3D 0)) =3D (A /=3D 0). Can't understand this... And I hav=
e tried  =

many things.

This second point may turn back into the first, saying =E2=80=9Cfinally,=
 if it  =

works fine using a language construct, why would you want to avoid to us=
e  =

this language construct ?=E2=80=9D, or alternatively to discuss this oft=
enly  =

occurring question : how do I make it understand such a simple thing... =
 =

without using user rules here.

Pleased to read you