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!border1.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!backlog2.nntp.dca.giganews.com!nntp.posted.plusnet!news.posted.plusnet.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 01 Apr 2009 18:50:45 -0500
Date: Thu, 02 Apr 2009 00:50:44 +0100
From: Tim Rowe <spamtrap@tgrowe.plus.net>
User-Agent: Thunderbird 2.0.0.21 (Windows/20090302)
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: Newbie question: SPARK verification condition on member of
 private
 record
References: <jsudnfEigqAgX07UnZ2dnUVZ8ridnZ2d@posted.plusnet>
 <cg$c+4BZb90JJwWv@diphi.demon.co.uk>
In-Reply-To: <cg$c+4BZb90JJwWv@diphi.demon.co.uk>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <et6dnUO6O_dLYE7UnZ2dnUVZ8o-dnZ2d@posted.plusnet>
X-Usenet-Provider: http://www.giganews.com
X-Trace: 
 sv3-D0rKMtDbaFYaeFaApIzf6CtKRSkwxqMBxldKuEtTtjrJXb4r7YH9GnT/Itc/TKAvFN0ml1R5trYApec!WiofI5XAe+lFk8QbCdzAnCl/VnZSJuee5UplA80JaLDr0J6xZm4FineFbm7nKyZp00s+MqGsVOrz!mIXNvQexm0Zk
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint
 properly
X-Postfilter: 1.3.39
X-Original-Bytes: 2333
Xref: g2news2.google.com comp.lang.ada:5368
Date: 2009-04-02T00:50:44+01:00
List-Id: <comp.lang.ada>

JP Thornley wrote:

> 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.

That works nicely, thanks. Although...

> 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.]

... I'll probably want to get around to that approach eventually. In 
fact, sooner rather than later I think. Otherwise for some of the other 
proof obligations it looks as if I'm going to need a lot of user rules 
to tell the simplifier that various operations don't affect the results 
of Get_Order. I had thought of proof functions but couldn't see how not 
to move the same problem into the proof function.

How long-winded is long-winded?