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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,af40877501f46910 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Path: g2news1.google.com!postnews.google.com!v41g2000yqv.googlegroups.com!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: SPARK understand me very well... me neither Date: Sat, 14 Aug 2010 09:04:23 -0700 (PDT) Organization: http://groups.google.com Message-ID: <2308d0a0-8fdb-41a0-b2dc-6b30a2bf2f18@v41g2000yqv.googlegroups.com> References: NNTP-Posting-Host: 80.177.171.182 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1281801863 23391 127.0.0.1 (14 Aug 2010 16:04:23 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Sat, 14 Aug 2010 16:04:23 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: v41g2000yqv.googlegroups.com; posting-host=80.177.171.182; posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64; Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR 3.0.30729; Media Center PC 6.0; .NET4.0C),gzip(gfe) Xref: g2news1.google.com comp.lang.ada:13286 Date: 2010-08-14T09:04:23-07:00 List-Id: On 14 Aug, 05:57, Yannick Duch=EAne (Hibou57) wrote: > I have looked at it again, and cannot do better than stopping here: > > =A0 =A0 package Functions is > =A0 =A0 =A0 =A0function Multiply (A, B : Natural) return Natural; > =A0 =A0 =A0 =A0--# pre (A /=3D 0) -> (B <=3D (Integer'Last / A)); > =A0 =A0 =A0 =A0--# return A * B; -- Implies commutativity on Multiply arg= uments > =A0 =A0 end Functions; > > =A0 =A0 package body Functions is > =A0 =A0 =A0 =A0function Multiply (A, B : Natural) return Natural > =A0 =A0 =A0 =A0is > =A0 =A0 =A0 =A0 =A0 Result : Natural; > =A0 =A0 =A0 =A0begin > =A0 =A0 =A0 =A0 =A0 --# check (A =3D 0) -> ((A * B) =3D 0); > =A0 =A0 =A0 =A0 =A0 --# check (A =3D 0) -> ((B * A) <=3D Integer'Last); > =A0 =A0 =A0 =A0 =A0 --# check not (A =3D 0) -> (B <=3D (Integer'Last / A)= ); > =A0 =A0 =A0 =A0 =A0 --# check not (A =3D 0) -> ((B * A) <=3D (Integer'Las= t / A) * A); > =A0 =A0 =A0 =A0 =A0 --# check not (A =3D 0) -> ((Integer'Last / A) * A <= =3D Integer'Last); > =A0 =A0 =A0 =A0 =A0 --# check not (A =3D 0) -> ((B * A) <=3D Integer'Last= ); > =A0 =A0 =A0 =A0 =A0 -- Here is a gap which I cannot cross > =A0 =A0 =A0 =A0 =A0 --# assert (A * B) <=3D Integer'Last; > =A0 =A0 =A0 =A0 =A0 Result :=3D A * B; > =A0 =A0 =A0 =A0 =A0 return Result; > =A0 =A0 =A0 =A0end Multiply; > =A0 =A0 end Functions; > [...] I'm going to question this way of completing proofs in SPARK. Yannick, I realise that you are an enthusiast for this but it's not the way that the job is done in practice - it doesn't scale up for real problems. When it takes seven proof statements to (fail to) prove a simple multiplication then this method isn't practicable for the sorts of expressions that appear in the real-world models of embedded systems. So we shouldn't be publicising this approach in sites such as Rossetta Code. For this particular example, I don't understand why you haven't used the obvious precondition: --# pre A * B in Integer; which not only removes the need for all those 'check' statements but also allows the function to have Integer parameters and return value (rather then being restricted to Natural). The version of the precondition that will work best (measured by leaving the lowest number of unproven VCs) depends on how the calling code ensures that it meets the precondition. The easiest way to achieve this (for general purpose functions like Multiply) is by having the subtypes of the parameters as constrained as possible, so, as long as the bounds on the two terms are small enough, meeting this simpler version of the precondition is automatic. With your version of the precondition, most calls of the function are likely to generate an unproven VC that the user then has to deal with. OTOH, if the bounds of the parameter subtypes can't ensure the precondition, then the program has to use a defensive check, in which case your version of the precondition may work better (if the defensive check is exactly that precondition). In a well-designed program, the subtype constraints should match the usage of the variables of the subtypes and I would expect defensive checks to be quite rare. (It could be argued that a defensive check indicates a failure - or at least a weakness - in the design.) They mainly occur as checks on values coming in across the system boundary. Where a defensive check is required then I would provide a user-rule that allows the relevant precondition to be proved from the check that is made. So I would much prefer the simple and obvious version of the precondition and code to be the version on Rosetta Code so that anyone browsing that site for information about SPARK doesn't get a wrong view of the language. Cheers, Phil