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,5bcfd29df81c93e0,start X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit X-Received: by 10.224.217.195 with SMTP id hn3mr3828915qab.5.1367397324447; Wed, 01 May 2013 01:35:24 -0700 (PDT) X-Received: by 10.49.12.15 with SMTP id u15mr84508qeb.21.1367397324427; Wed, 01 May 2013 01:35:24 -0700 (PDT) Path: ef9ni38601qab.0!nntp.google.com!s14no1534873qam.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Wed, 1 May 2013 01:35:24 -0700 (PDT) Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=79.205.216.43; posting-account=FZSaEQoAAAAXdVQbBo8KLQ8RHCBHvDzm NNTP-Posting-Host: 79.205.216.43 User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <0efb385b-279a-49b7-8289-86b0e99e7930@googlegroups.com> Subject: SPARK Question From: "M. Enzmann" Injection-Date: Wed, 01 May 2013 08:35:24 +0000 Content-Type: text/plain; charset=ISO-8859-1 Date: 2013-05-01T01:35:24-07:00 List-Id: Hi all, I have a question regarding post- and pre-conditions for subprograms that use private types as arguments / return values. I am trying the following: I want to encapsulate a vector type in a private tagged record. Attempting to access "internals" of the tagged type in PRE / POST annotations is then clearly not feasible. I can use getter / setter functions in the annotations, there is however a problem regarding the sequence in which I declare these subprograms. I read in the Proof-Manual, that I should be using proof-functions, yet I am not quite sure I know how to do this. Especially the part about writing rules for the given proof-function is hard to grasp for me... Let me clarify what I want to do using an example: First I declare an unconstrained vector-type, then I declare an constrained type, that is then being encapsulated in the tagged type. > Number_Of_Elements : constant Positive := 100; > subtype Basis_Type is Float; > > -- ----------------------------------------------------------------------- > -- Type declarations > -- ----------------------------------------------------------------------- > > -- declare an unconstrained array to exchange vectors of different sizes > type Uncon_Array is array (Positive range <>) of Basis_Type; > > -- define the range of the array index > subtype Array_Range is Integer range 1 .. Number_Of_Elements; > > -- array constrained to the index range > subtype Basic_Array is Uncon_Array (Array_Range); > > -- declare the primary vector type as tagged private record > type Basic_Vector is tagged private; and in the private part > type Basic_Vector is tagged > record > Values : Basic_Array; > Length : Natural; > end record; The vector can now hold a maximum of "Number_Of_Elements" Values, although the actually used length will in most cases be smaller. This "true" length is shown by the component "Length" in the record. Reading a single element of the vector now needs a function > function Get_Value > (The_Vector : in Basic_Vector; > At_Position : in Positive) > return Basis_Type; > --# PRE At_Position in Array_Range; which clearly will not work if "At_Position" is larger than "Number_Of_Elements". Furthermore it will however not give a useful result, if "At_Position" is larger than "The_Vector.Length". How can I express this in a pre-condition? I can write a function > function Vector_Length (The_Vector : in Basic_Vector) return Positive; and use this in the pre-condition. This leaves however a couple of questions open, so I'd prefer to do this in a different way. As far as I understand, a proof-function > --# function Vec_Length (The_Vector : in Basic_Vector) return Positive; could do the trick in the specification and a more elaborate version of the pre-condition will then be used in the body. I have however no idea, how the two are linked and how I can express the relationship in the rules file. Any help will be appreciated! TIA, Marc