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,48e1a3c594fb62e8
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,UTF8
Path: 
 g2news2.google.com!news4.google.com!proxad.net!feeder1-2.proxad.net!usenet-fr.net!gegeweb.org!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: SPARK
Date: Sat, 15 May 2010 18:41:05 +0200
Organization: Ada At Home
Message-ID: <op.vcq9yrdhule2fv@garhos>
References: <op.vcl6900wule2fv@garhos>
NNTP-Posting-Host: sTlYSXnTcjJGTYbLtvdIYA.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.53 (Win32)
Xref: g2news2.google.com comp.lang.ada:11637
Date: 2010-05-15T18:41:05+02:00
List-Id: <comp.lang.ada>

Currently, I'm reading Phil's documents, the ones in the directory  =

Proof_Annotations and especially looking at exercises (yes, he created  =

some) in part 5 to 9 and 12.

Part 5, exercise 4, turns to be something interesting to me, as it leads=
  =

me to some questions about the way the simplifier is using hypothesis.

I would like to be more explicit. Here is the relevant part (slightly  =

modified)


    --------------------------------------------------------------------=
-
    -- Exercise 5.4
    --------------------------------------------------------------------=
-
    procedure Limit
      (X     : in out Integer;
       Lower : in     Integer;
       Upper : in     Integer)
    --# pre    Lower < Upper;
    --# post  ((X~ < Lower) -> (X =3D Lower)) and
    --#       ((X~ > Upper) -> (X =3D Upper)) and
    --#       (X in Lower .. Upper);
    is
    begin
       if X < Lower then
          X :=3D Lower;
       elsif X > Upper then
          X :=3D Upper;
       end if;
    end Limit;

    function Percent_Of_Range
      (Data    : Integer;
       Lowest  : Integer;
       Highest : Integer) return Percent_Type
    --# pre    (Lowest < Highest) and                        -- (1)
    --#        ((Highest - Lowest) <=3D Integer'Last) and      -- (2)
    --#        (((Highest - Lowest) * 100) <=3D Integer'Last); -- (3)
    --#
    is
       Local_Data : Integer;
       Part : Integer;
       Whole : Integer;
    begin
       Local_Data :=3D Data;                                   -- (4)
       Limit (Local_Data, Lowest, Highest);                  -- (5)
       Part :=3D Local_Data - Lowest;                          -- (6)
       Whole :=3D Highest - Lowest;                            -- (7)
       return Percent_Type((Part * 100) / Whole);            -- (8)
    end Percent_Of_Range;


What's funny here, is about precondition line (2). If it is removed, the=
  =

precondition become =E2=80=9C(Lowest < Highest) and (((Highest - Lowest)=
 * 100) <=3D  =

Integer'Last)=E2=80=9D and the simplifier fails to prove line (6) : it c=
annot  =

prove the result will be lower than Integer'Last. I first though =E2=80=9C=
(Highest  =

- Lowest) * 100 <=3D Integer'Last=E2=80=9D would be enough to also impli=
es =E2=80=9CHighest  =

- Lowest < Integer'Last=E2=80=9D ; it seems it is not. If you add precon=
dition  =

part (2), there is no more trouble with line (6).

Is this because of the way it is using hypotheses or is this because it =
 =

miss some built-in rules to get all benefits from precondition part (3) =
?

Now, there is still another unproved condition... at line (8), the  =

simplifier cannot prove =E2=80=9C((Local_Data - Lowest) * 100) / (Highes=
t -  =

Lowest) <=3D 100=E2=80=9D. A first anecdote : funny to see it has expand=
ed variables  =

Part and Whole.

I wanted to solve in three steps and added the following between (6) and=
  =

(7)


       --# assert Part <=3D Whole; -- (6.1)
       --# assert (Part * 100) <=3D (Whole * 100); -- (6.2)
       --# assert ((Part * 100) / Whole) <=3D ((Whole * 100) / Whole); -=
-  =

(6.3)


But the simplifier was not able to prove (6.1) nor (6.3) and was still n=
ot  =

able to prove (8). About (6.2), and wanted to have a test, and added the=
  =

following between (6.2) and (6.3):


       --# assert ((Part * 100) <=3D (Whole * 100)) ->
       --#        (((Part * 100) / Whole) <=3D ((Whole * 100) / Whole));=



It was not able to prove it. Do I miss something or does it simply means=
  =

the simplifier does not know about a rule which seems basic to me, that =
is  =

(A <=3D B) -> ((A / C) <=3D (B / C)) ? ... which is still valid for inte=
ger  =

arithmetic.

-- =

There is even better than a pragma Assert: an --# assert