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 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,e6cf7d66027047db X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news1.google.com!npeer03.iad.highwinds-media.com!feed-me.highwinds-media.com!cyclone03.ams2.highwinds-media.com!news.highwinds-media.com!npeersf01.ams.highwinds-media.com!newsfe24.ams2.POSTED!7564ea0f!not-for-mail Message-ID: From: JP Thornley Newsgroups: comp.lang.ada Subject: Re: Newbie question: SPARK verification condition on member of private record References: MIME-Version: 1.0 Content-Type: text/plain;charset=us-ascii;format=flowed User-Agent: Turnpike/6.07-S (<5rwliimRas86wQFOKvacArbuis>) NNTP-Posting-Host: 80.177.171.182 X-Complaints-To: abuse@demon.net X-Trace: newsfe24.ams2 1238619880 80.177.171.182 (Wed, 01 Apr 2009 21:04:40 UTC) NNTP-Posting-Date: Wed, 01 Apr 2009 21:04:40 UTC Date: Wed, 1 Apr 2009 22:04:25 +0100 Xref: g2news2.google.com comp.lang.ada:5367 Date: 2009-04-01T22:04:25+01:00 List-Id: In article , Tim Rowe writes >Ok, I've been busily reading all of the spark documentation, and >there's just one thing I'm stuck on at the moment. > >I have: > subtype Array_Index is Integer range 1..5000; > type Foo is private; > function Get_Order(This: in Foo) return Array_Index; > -- other specifications > >and in the private part I have > type Foo is record > Highest_Valid_Index: Array_Index; > -- other definitions > end record; > >The body of Get_Order is simply > function Get_Order(This: in Foo) return Array_Index is > begin > return This.Highest_Valid_Index; > end Get_Order; > >My problem is that I'm getting a proof obligation >H1: get_order(this) < 5000 . >C1: fld_highest_valid_index(this) <= 4999 . >If I'm reading that correctly then it's clearly true, but I would like >to be able to annotate the code so that Examiner knows that >get_order(this) = fld_highest_valid_index(this). My instinct is to >annotate Get_Order with > --# return This.Highest_Valid_Index; >but that's not allowed (" Semantic Error : 9: Selected components >are not allowed for This.") > >So how should I annotate or restructure the code to make the >relationship between Get_Order(This) and This.Highest_Valid_Index? The easiest way to deal with this is to create a user rule to replace get_order(X) with fld_highest_valid_index(X): The rule should look like: a_name(1): get_order(X) may_be_replaced_by fld_highest_valid_index(X). where 'a_name' can be any name you like. X will be treated as a wildcard that matches to anything in the VC. The justification for the rule is the code of the function Get_Order. It really would be nice to have a return annotation on the function but, as you have found, this isn't possible with private types. [Actually it is possible, but very longwinded and involves the additional definition of a proof function, so it isn't usually considered worthwhile for such simple code.] The name of the rule file must be X.rlu where X is either the name of the operation that the VC is generated by or the name of the package that the operation is in. The file must appear in the folder containing the vcg etc. files of the operation. (When the Simplifier starts on a file op_name.vcg in folder pack_name it looks for user rule files called op_name.rlu and pack_name.rlu, so op_name.rlu should have rules that are specific to the operation and pack_name.rlu should have rules that are applicable throughout the package.) If this doesn't work then you may need a more specific rule, such as a_name(2): fld_highest_valid_index(X) <= 4999 may_be_deduced_from [ get_order(X) < 5000 ]. with the same justification. Hope this helps - for more info read section 7 of the Simplifier User Manual which is all about user rules. Cheers, Phil -- JP Thornley