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: a07f3367d7,ec6f74e58e86b38b
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.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: Re: Lost in translation (with SPARK user rules)
Date: Tue, 01 Jun 2010 07:42:20 +0200
Organization: Ada At Home
Message-ID: <op.vdlwsuajule2fv@garhos>
References: <op.vda45rsfule2fv@garhos>
NNTP-Posting-Host: vjyChO3Bz9QTYTXyWN6Pgw.user.speranza.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes
Content-Transfer-Encoding: 7bit
X-Complaints-To: abuse@aioe.org
X-Notice: Filtered by postfilter v. 0.8.2
User-Agent: Opera Mail/10.53 (Win32)
Xref: g2news2.google.com comp.lang.ada:12168
Date: 2010-06-01T07:42:20+02:00
List-Id: <comp.lang.ada>

A little test I did right a few seconds ago.

Let a rule be of the form:

    C1 may_be_deduced_from [C2, V].

Which is so that this one is valid too:

    C2 may_be_deduced_from [C1, V].

So finally, C1 and C2 and both either conclusion or condition.

This may *logically* (not by pattern) match three other things:

    C1  -> C2 may_be_deduced_from [V].
    C2  -> C1 may_be_deduced_from [V].
    C1 <-> C2 may_be_deduced_from [V].

Although only one would be required, which is

    C1 <-> C2 may_be_deduced_from [V].

Instead one need to have (and write) all of:

    C1 may_be_deduced_from [C2, V].
    C2 may_be_deduced_from [C1, V].
    C1  -> C2 may_be_deduced_from [V].
    C2  -> C1 may_be_deduced_from [V].
    C1 <-> C2 may_be_deduced_from [V].

Five rules instead of one, where one logical rule would be sufficient.

I wanted to get ride of this, with these generic rules, which I hoped will  
help and solve this recurrent trick:

    A may_be_deduced_from [B, B -> A].
    A may_be_deduced_from [B, B <-> A].
    B may_be_deduced_from [A, B <-> A].
    B -> A may_be_deduced_from [B <-> A].
    A -> B may_be_deduced_from [B <-> A].

I though this would ends to exact matches, and I would have only to write  
rules of the form

    C1 <-> C2 may_be_deduced_from [V].
    ... <-> ... may_be_deduced_from [...].

or of the form

    C1 -> C2 may_be_deduced_from [V].
    ... -> ... may_be_deduced_from [...].

and expected I would have to write only this, avoiding duplications of  
multiple equivalent forms (I expected these equivalent forms would be  
deduced via the above generic rules). Unfortunately, and although this  
looks like there should be exact matches after instantiations, this does  
not work (rules does not match in Simplifier).

Now I really see why there is the restriction of user rules which are to  
be defined on package or subprogram basis (while I still don't enjoy this)  
: this test clearly demonstrate there is no way to write general rules,  
these are always specifics to a VC or a set of VC for a given package or  
subprogram. Or else, all logical equivalences need to be written  
explicitly (which in turn requires great care when one want to review  
rules, as duplication -- I know it after experiences -- does not help  
safety and help to miss weakness).

Note: SPARK is still useful ;) with these words, I don't wanted to say it  
is not good


-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.