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!news2.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: Thu, 02 Apr 2009 07:00:30 -0500 Date: Thu, 02 Apr 2009 13:00:28 +0100 From: Tim Rowe 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: In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Message-ID: X-Usenet-Provider: http://www.giganews.com X-Trace: sv3-dMHalutOkEPxn2us/Tyz9Axo0z8NoxNxi+G0nvKkf1c4wv/3zBM4DtAx614XQhv58Bb1Sth6JCNdrwc!au2gSYtJus/zZo/2OsFQ4MHKmeDoUiN0zv5a6zy/BKPrFag8C8/kSWNFaNUMD6vjb4c8pszO7l70!+6KtgnoQV43v 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: 5108 Xref: g2news2.google.com comp.lang.ada:5370 Date: 2009-04-02T13:00:28+01:00 List-Id: JP Thornley wrote: > However I would never recommend degrading the software structure to make > proof easier - at least for proof of absence of run-time error (proof of > partial correctness may be a different matter). The other proof obligations I'm getting /are/ for partial correctness. An operation that changes a lot of fields in the private record has a postcondition describing what the effect should be on each field. But I can only describe that effect in terms of the Get_xxx functions. That means that, for instance, the postcondition on Get_Order is padded with a lot of stuff about the updating of fields that have no effect on Get_Order. > In this case you may need to add postconditions on various operations > that update objects of the private type, to say that the result of > Get_Order is unchanged by the operation, but this is probably better > than the alternative - which is make the type visible. Unfortunately, the fields of the private type are related, so they all change together for consistency. Maybe I should get more specific. As a tutorial exercise, I'm looking at what an existing program for transforming the format of a fault tree report file would look like in SPARK -- not with the intention of using it, but so that I understand SPARK better. So the private type in question is: type Cut_Set is record Probability : Probability_Type; Events : Event_Array_Type; Highest_Valid_Index : Array_Index; end record; and I add an event to the cutset with procedure Add (This : in out Cut_Set; Conjunction : in Event_Conjunctions.Event_Conjunction); --# derives This from *, --# Conjunction; --# pre Get_Order(This) < Array_Index'Last and --# 1.0 - Get_Probability(This) >= --# Event_Conjunctions.Get_Probability(Conjunction); --# --# post (Get_Order(This) = Get_Order(This~) + 1) and --# (for all I in Array_Index range Array_Index'First..Get_Order(This~) --# => (Get_Conjunction(This, I) = Get_Conjunction(This~, I))) and --# Get_Conjunction(This, Get_Order(This)) = Conjunction and --# Get_Probability(This) = --# Get_Probability(This~) + --# Event_Conjunctions.Get_Probability(Conjunction); (As previously mentioned, Get_Order returns Highest_Valid_Index, and yes, I am aware of the issues with testing for equality on floats and that I have a hidden assumption that Array_Index'First = 1). That's giving me conclusions to prove like: H1: get_order(this) < 5000 . H2: 1 - get_probability(this) >= event_conjunctions__get_probability( conjunction) . H3: fld_highest_valid_index(this) >= 1 . H4: fld_highest_valid_index(this) <= 4999 . -> C1: get_order(upf_probability(upf_events(upf_highest_valid_index(this, fld_highest_valid_index(this) + 1), update(fld_events(this), [ fld_highest_valid_index(this) + 1], conjunction)), fld_probability( this) + event_conjunctions__get_probability(conjunction))) = get_order(this) + 1 . That's one of the easier ones. The point is that upf_probability, upf_events and update can't affect the result of get_order. Knowing that I can reduce the espression to get_order( upf_highest_valid_index ( this, fld_highest_valid_index(this) + 1 ) ) = get_order(this) + 1 which I can prove easily enough, but the process seems error prone (as I say, this is one of the simpler ones). If I /could/ give the tools some hints to reduce it it would be a big help. Maybe I /should/ make the record public! If nothing else, I found an error in the postcondition by explaining this ;-)