From: "M. Enzmann" <enzmann.m@googlemail.com>
Subject: SPARK Question
Date: Wed, 1 May 2013 01:35:24 -0700 (PDT)
Date: 2013-05-01T01:35:24-07:00 [thread overview]
Message-ID: <0efb385b-279a-49b7-8289-86b0e99e7930@googlegroups.com> (raw)
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
next reply other threads:[~2013-05-01 8:35 UTC|newest]
Thread overview: 13+ messages / expand[flat|nested] mbox.gz Atom feed top
2013-05-01 8:35 M. Enzmann [this message]
2013-05-01 13:35 ` SPARK Question Phil Thornley
2013-05-07 6:59 ` Yannick Duchêne (Hibou57)
2013-05-07 7:54 ` Georg Bauhaus
2013-05-07 20:44 ` Jacob Sparre Andersen news
2013-05-19 18:54 ` phil.clayton
2013-05-20 23:40 ` Randy Brukardt
2013-05-02 5:48 ` M. Enzmann
-- strict thread matches above, loose matches on Subject: below --
2018-08-27 14:10 SPARK question Simon Wright
2018-08-27 16:39 ` Shark8
2018-08-27 20:19 ` Simon Wright
2018-08-27 21:36 ` Randy Brukardt
2018-08-28 19:05 ` Simon Wright
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox