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!news3.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?= Newsgroups: comp.lang.ada Subject: Re: SPARK Date: Sat, 15 May 2010 22:23:31 +0200 Organization: Ada At Home Message-ID: References: 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:11644 Date: 2010-05-15T22:23:31+02:00 List-Id: Le Sat, 15 May 2010 21:08:05 +0200, Yannick Duch=C3=AAne (Hibou57) = a =C3=A9crit: > Oh, something interesting: > > > 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); > > -- ..... > > > Limit (Local_Data, Lowest, Highest); > --# assert Local_Data <=3D Highest; -- (1) > Part :=3D Local_Data - Lowest; > Whole :=3D Highest - Lowest; > --# assert Part >=3D 0; -- (2) > --# assert Local_Data <=3D Highest; -- (3) > > -- ..... > > > If (2) is removed, it can prove (1) and (3). If (2) is there, it fails= = > to prove (3), while nothing changes Local_Data in the path from (1) to= = > (3), and so (3) should be as much provable as (1). If =E2=80=9Cassert=E2=80=9D is replaced by =E2=80=9Ccheck=E2=80=9D then = it can prove (3) even if (2) is = there. So that 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); -- ..... Limit (Local_Data, Lowest, Highest); --# check Local_Data <=3D Highest; -- (1) Part :=3D Local_Data - Lowest; Whole :=3D Highest - Lowest; --# check Part >=3D 0; -- (2) --# check Local_Data <=3D Highest; -- (3) -- ..... is OK. So let's talk about =E2=80=9Cassert=E2=80=9D vs =E2=80=9Ccheck=E2=80=9D.= [Generation of VCs for SPARK Programs (2.2)] says: > each assert or check statement in the code is located at a point in > between two executable statements, in general, ie it is associated > with a point on the arc of the flowchart of the subprogram which > passes between the two statements it appears between. Each such > assertion specifies a relation between program variables which must > hold at that precise point, whenever execution reaches it. Assert > statements generate a cut point on the flowchart of the subprogram, > check statements do not. What does =E2=80=9Ccut point=E2=80=9D means precisely ? Is it related or= similar to the = unfortunately too much famous Prolog's cut ? This seems to be the next = question to be answered, and a focus to care about for peoples learning = = SPARK. Is that this =E2=80=9Ccut point=E2=80=9D which makes Simplifier to forge= t about previous = hypotheses when =E2=80=9Cassert=E2=80=9D is used ? (if that's really sim= ilar to Prolog's = cut, then indeed, it likely to make the prover loose memory) About one of the most worthy thing with proving : what's the better way = to = give hints to the prover ? Is it =E2=80=9Cassert=E2=80=9D or =E2=80=9Cch= eck=E2=80=9D ? This example = suggest the best way is =E2=80=9Ccheck=E2=80=9D. Is this example represe= ntative of most = cases or a just a special case ? -- There is even better than a pragma Assert: an --# assert (or a --# = check.... question pending)