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,d4e6b104ff087788 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Path: g2news1.google.com!news3.google.com!feeder2.cambriumusenet.nl!feed.tweaknews.nl!194.134.4.91.MISMATCH!news2.euro.net!news.mixmin.net!aioe.org!not-for-mail From: =?iso-8859-15?Q?Yannick_Duch=EAne_=28Hibou57=29?= Newsgroups: comp.lang.ada Subject: Re: SPARK : surprising failure with implication Date: Thu, 03 Jun 2010 10:54:51 +0200 Organization: Ada At Home Message-ID: References: NNTP-Posting-Host: o1huFJB2ANcHlWoNFASSiA.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-15; 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.53 (Win32) Xref: g2news1.google.com comp.lang.ada:11248 Date: 2010-06-03T10:54:51+02:00 List-Id: Le Wed, 02 Jun 2010 10:50:55 +0200, Yannick Duch=EAne (Hibou57) = a =E9crit: > Not exactly with implication this time, this is about equality and = > substitution. > > Here is a case I am facing (simplified for the purpose of this message= ): > > --# assert S =3D (I / X); -- (1) > --# check S =3D T'Pos (S); -- (2) > --# check I =3D T'Pos (I); -- (3) > --# check T'Pos (S) =3D (T'Pos (I) / X); -- (4) > > (1) is proved > (2) and (3) are proved > Simplifier fails to prove (4) despite of (1) and equalities (2) and (3= ) = > which should be used to substitute S and I in (1). > > I still did not found a workaround for this one (I am busy at this now= ). > > Does anyone already meet a case similar to this one ? Does it fails fo= r = > the reason it requires two substitutions at a time ? A example which made me think about this one, while different. This time= , = there is only one substitution, and it still fails. First, the case (extract from an *.SIV file): C1: instance mod 2 ** (result + 1) * 2 ** (7 - result) * 2 mod 25= 6 =3D instance mod 2 ** (result - 1 + 2) * 2 ** (7 - result) * 2= = mod 256 . And its precursor as it appears in the *.VCG file: C1: source * 2 mod instance_type__modulus =3D instance mod base ** (result - 1 + 2) * base ** (u__last - ( result - 1 + 1)) * 2 mod base ** (u__last + 1) . This conclusion could not be proved, because it fails to simplify (resul= t = - 1 + 2) into (result + 1), and I've checked it also fails to substitute= = (result - 1 + 2) to (result + 1). I have tried many thing, including a = user rule like this one as my last attempt: my_test(1): A - 1 + 2 may_be_replaced_by [ A + 1 ]. As well as my_test(2): (A - 1) + 2 may_be_replaced_by [ A + 1 ]. Without success. The original context in Ada/SPARK source is of the form (the above C1 = stands for the Check clause): --# assert ..... U'Pos (Result + 1) ..... ..... Result :=3D Result + 1; ..... --# check .... U'Pos (Result + 1 + 1) .... I suspect it to see Result - 1, standing for the value of Result in the = = Assert clause (and thus as the actual expression standing for Result), a= s = a monolithic subexpression. If this is really what happens, then it woul= d = not see (Result + 1 + 1) as (Result - 1 + 1 + 1), and instead as ((Resul= t = - 1) + 1 + 1), then see 1 + 1 as an expression, which is simplifies to 2= , = getting ((Result - 1) + 2), which it could not simplify any more, as it = = could not see -1 + 2 as a simplifiable expression, because -1 belongs to= a = subexpression. However, what it strange, it that Result - 1 does not appears as a = subexpression in neither the SIV file nor the VCG file. So I wonder if = this is really the explanation of what's going on. Further more, the two= = attempt with above user rules, did not solve anything. Both simplificati= on = of a constant expression and substitution fails here. Probably needs even more investigation. -- = 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.