SPARK Question

SPARK Question

[M. Enzmann]

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

Re: SPARK Question

[Phil Thornley]

In article <0efb385b-279a-49b7-8289-86b0e99e7930@googlegroups.com>, 
enzmann.m@googlemail.com says...

[snip]

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

Assuming you are using the latest version of SPARK, the simplest way to 
do this is to also include the proof function Vec_Length in the body, 
and give it a return annotation. So in the spec put:

   --# function Vec_Length (The_Vector : in Basic_Vector)
   --#   return Positive;

   function Get_Value
     (The_Vector : in Basic_Vector;
      At_Position : in Positive)
      return Basis_Type;
   --# PRE At_Position in Array_Range'First .. Vec_Length(The_Vector);

and in the body put:

   --# function Vec_Length (The_Vector : in Basic_Vector)
   --#   return Positive;
   --# return The_Vector.Length;

With the other code as you have it in your post, this leaves one 
unprovable VC for Get_Value, as the value of Length in the record is 
declared as Natural.  If  this is changed to Array_Range it makes the VC 
provable, and proved by the Simplifier. (But this then means that you 
cannot have an empty vector - which can be fixed by declaring another 
subtype for Length that includes 0).

You need to be aware that by doing it this way rather than having a 
coded function for Vec_Length (which you say you don't want to do) you 
are making a claim for Vec_Length that cannot be validated by the proof 
tools.  (See section 3.3 of the document "Calling functions in SPARK 
proof contexts").

Cheers,

Phil

Re: SPARK Question

[M. Enzmann]

Phew! VCs are tough cookies. For me at least...

Thanks for the help Phil!

Re: SPARK Question

[Yannick Duchêne (Hibou57)]

Le Wed, 01 May 2013 15:35:20 +0200, Phil Thornley  
<phil.jpthornley@gmail.com> a écrit:
> Assuming you are using the latest version of SPARK, the simplest way to
> do this is to also include the proof function Vec_Length in the body,
> and give it a return annotation. So in the spec put:
>
>    --# function Vec_Length (The_Vector : in Basic_Vector)
>    --#   return Positive;
>
>    function Get_Value
>      (The_Vector : in Basic_Vector;
>       At_Position : in Positive)
>       return Basis_Type;
>    --# PRE At_Position in Array_Range'First .. Vec_Length(The_Vector);
>

That's exactly the kind of thing I miss with Ada 2012's Pre/Post: ability  
to define something for use in pre/post only, without injecting it in the  
real program. That's finally what the above do.

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: SPARK Question

[Georg Bauhaus]

On 07.05.13 08:59, Yannick Duchêne (Hibou57) wrote:
> Le Wed, 01 May 2013 15:35:20 +0200, Phil Thornley <phil.jpthornley@gmail.com> a écrit:
>> Assuming you are using the latest version of SPARK, the simplest way to
>> do this is to also include the proof function Vec_Length in the body,
>> and give it a return annotation. So in the spec put:
>>
>>    --# function Vec_Length (The_Vector : in Basic_Vector)
>>    --#   return Positive;
>>
>>    function Get_Value
>>      (The_Vector : in Basic_Vector;
>>       At_Position : in Positive)
>>       return Basis_Type;
>>    --# PRE At_Position in Array_Range'First .. Vec_Length(The_Vector);
>>
>
> That's exactly the kind of thing I miss with Ada 2012's Pre/Post: ability to define something for use in pre/post only, without injecting it in the real program. That's finally what the above do.
>

In practical cases, contract-only predicates might well vanish
during optimization phases in compilers, I think, in case the
programmers decide that assertion checking can be turned off.

Re: SPARK Question

[Jacob Sparre Andersen news]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 2699 bytes --]

"Georg Bauhaus" <rm.dash-bauhaus@futureapps.de> wrote in message 
news:5188b317$0$6555$9b4e6d93@newsspool4.arcor-online.net...
> On 07.05.13 08:59, Yannick Duchêne (Hibou57) wrote:
>> Le Wed, 01 May 2013 15:35:20 +0200, Phil Thornley 
>> <phil.jpthornley@gmail.com> a écrit:
>>> Assuming you are using the latest version of SPARK, the simplest way to
>>> do this is to also include the proof function Vec_Length in the body,
>>> and give it a return annotation. So in the spec put:
>>>
>>>    --# function Vec_Length (The_Vector : in Basic_Vector)
>>>    --#   return Positive;
>>>
>>>    function Get_Value
>>>      (The_Vector : in Basic_Vector;
>>>       At_Position : in Positive)
>>>       return Basis_Type;
>>>    --# PRE At_Position in Array_Range'First .. Vec_Length(The_Vector);
>>>
>>
>> That's exactly the kind of thing I miss with Ada 2012's Pre/Post: ability 
>> to define something for use in pre/post only, without injecting it in the 
>> real program. That's finally what the above do.
>>
>
> In practical cases, contract-only predicates might well vanish
> during optimization phases in compilers, I think, in case the
> programmers decide that assertion checking can be turned off.

I agree. Compilers do not include dead code in programs, regardless of why 
that code is dead. So there is little practical difference between having 
some sort of contract-only predicate functions and having them generally 
available.

Moreover, I'm very skeptical that having contract-only functions is a good 
idea, especially for preconditions. For a precondition, the caller is 
supposed to ensure that the precondition is true before making the call. How 
can a programmer do this if the predicate is not available to them? For 
instance, it's common to have code like:

    if Is_Open (Log_File) then
        Put_Line (Log_File, ...);
    -- else don't log, file has failed for some reason.
    end if;

where the precondition on Put_Line includes "Is_Open (File)".

If the programmer can't write Is_Open in their code, they cannot avoid the 
failure nor program around it. All they can do is handle the exception, 
which is often the worst way to handle the situation.

Similarly, postconditions often include conditions that hold true after the 
call, and it's quite common for those conditions to feed into following 
preconditions (as in Post => Is_Open(File) after a call to Open). So, as 
much as possible, postconditions should use the same functions that are used 
in preconditions. (The more that's done, the more likely that the compiler 
can completely eliminate the pre- and post- condition checks even when 
they're turned on.)

                                        Randy.

Re: SPARK Question

[phil.clayton]

On Tuesday, 7 May 2013 21:44:12 UTC+1, Jacob Sparre Andersen news  wrote:
> "Georg Bauhaus" <...@futureapps.de> wrote in message 
> news:...@newsspool4.arcor-online.net...
> > On 07.05.13 08:59, Yannick Duch�ne (Hibou57) wrote:
> >> Le Wed, 01 May 2013 15:35:20 +0200, Phil Thornley 
> >> <...@gmail.com> a �crit:
> >>> Assuming you are using the latest version of SPARK, the simplest way to
> >>> do this is to also include the proof function Vec_Length in the body,
> >>> and give it a return annotation. So in the spec put:
> >>>
> >>>    --# function Vec_Length (The_Vector : in Basic_Vector)
> >>>    --#   return Positive;
> >>>
> >>>    function Get_Value
> >>>      (The_Vector : in Basic_Vector;
> >>>       At_Position : in Positive)
> >>>       return Basis_Type;
> >>>    --# PRE At_Position in Array_Range'First .. Vec_Length(The_Vector);
> >>>
> >>
> >> That's exactly the kind of thing I miss with Ada 2012's Pre/Post: ability 
> >> to define something for use in pre/post only, without injecting it in the 
> >> real program. That's finally what the above do.
> >>
> >
> > In practical cases, contract-only predicates might well vanish
> > during optimization phases in compilers, I think, in case the
> > programmers decide that assertion checking can be turned off.
> 
> I agree. Compilers do not include dead code in programs, regardless of why 
> that code is dead. So there is little practical difference between having 
> some sort of contract-only predicate functions and having them generally 
> available.
> 
> Moreover, I'm very skeptical that having contract-only functions is a good 
> idea, especially for preconditions. For a precondition, the caller is 
> supposed to ensure that the precondition is true before making the call. How 
> can a programmer do this if the predicate is not available to them? For 
> instance, it's common to have code like:
> 
>     if Is_Open (Log_File) then
>         Put_Line (Log_File, ...);
>     -- else don't log, file has failed for some reason.
>     end if;
> 
> where the precondition on Put_Line includes "Is_Open (File)".
> 
> If the programmer can't write Is_Open in their code, they cannot avoid the 
> failure nor program around it. All they can do is handle the exception, 
> which is often the worst way to handle the situation.
> 
> Similarly, postconditions often include conditions that hold true after the 
> call, and it's quite common for those conditions to feed into following 
> preconditions (as in Post => Is_Open(File) after a call to Open). So, as 
> much as possible, postconditions should use the same functions that are used 
> in preconditions. (The more that's done, the more likely that the compiler 
> can completely eliminate the pre- and post- condition checks even when 
> they're turned on.)

Addressing the last paragraph above, the basis of the point is that reusing the same syntactic form of predicate in pre- and postconditions makes it easy for a compiler to spot that a predicate is a consequence of an earlier predicate.  I certainly agree with that!  But surely this would allow only the _subsequent_ occurrences of the predicate to be optimized out?  Above, you seem to suggest that both the initial and subsequent occurrence of a predicate can be optimized out.  In the example above example, it may be possible for the initial occurrence, the postcondition Is_Open(File) of subprogram Open, to be optimized out but that is surely for different reasons - the compiler having special knowledge about the subprogram Open.  In general, for user-defined subprograms, determining statically whether a predicate P(X) holds is, in general, difficult.  Once established, it is straightforward to use the theorem 
  P(X) ⇒ P(X)
to establish that subsequent occurrences of the same form hold.

Separately, even when reusing the same syntactic form of predicate in pre- and postconditions, optimizing out subsequent occurrences of the predicate may not be possible as often as one would hope.  Given two occurrences of the predicate P(X), to establish that the subsequent occurrence holds, it necessary (for the theorem above) to establish that the X is the same in both occurrences.  In the case that X is visible outside its package and between the two occurrences of P(X) there is a call to a subprogram in another package, I can't see how a compiler would know that X won't be changed.  (I'm assuming that compilers don't look at the bodies of other packages when compiling a package.)  To avoid such issues, formal methods tools typically require subprograms to have a 'frame' annotation that indicates which variables a subprogram may change.

So, in summary, optimizing out predicates in pre- and postconditions may not be that easy.

Phil

Re: SPARK Question

[Randy Brukardt]

<phil.clayton@lineone.net> wrote in message 
news:68e3b5b0-db45-4aeb-b6c4-817fe6845e5e@googlegroups.com...
On Tuesday, 7 May 2013 21:44:12 UTC+1, Randy Brukardt wrote:
...
>> Similarly, postconditions often include conditions that hold true after 
>> the
>> call, and it's quite common for those conditions to feed into following
>> preconditions (as in Post => Is_Open(File) after a call to Open). So, as
>> much as possible, postconditions should use the same functions that are 
>> used
>> in preconditions. (The more that's done, the more likely that the 
>> compiler
>> can completely eliminate the pre- and post- condition checks even when
>> they're turned on.)

>Addressing the last paragraph above, the basis of the point is that reusing 
>the
>same syntactic form of predicate in pre- and postconditions makes it easy 
>for a
>compiler to spot that a predicate is a consequence of an earlier predicate. 
>I
>certainly agree with that!  But surely this would allow only the 
>_subsequent_
>occurrences of the predicate to be optimized out?  Above, you seem to 
>suggest
>that both the initial and subsequent occurrence of a predicate can be 
>optimized out.

You're right that only the "subsequent" occurrences can be optimized out - 
but, in well-designed abstractions, the initial state also has a well-known 
set of predicates. This might be hard to model in Ada 2012, although 
invariants certainly would help. Starting out with undefined properties is 
not a good idea, so the only issue is whether there is a clear way to 
communicate that.

For instance, a file starts out with Is_Open = False. The compiler and 
static analyzer need to know this! It's too late to wait until Open is 
called.

> In the example above example, it may be possible for the initial 
> occurrence,
> the postcondition Is_Open(File) of subprogram Open, to be optimized out
> but that is surely for different reasons - the compiler having special 
> knowledge
> about the subprogram Open.

Postconditions get optimized out based on the actual contents of the body. 
This sort of optimization should be trivial (it is made with complete 
knowledge of the implementation, presuming the implementation is contained 
in a single package body, which normally should be the case). At the call 
site, they're assumptions (they've either been checked or proved, either way 
you don't need to recheck them).

> In general, for user-defined subprograms, determining statically whether a
> predicate P(X) holds is, in general, difficult.  Once established, it is
> straightforward to use the theorem  P(X) ? P(X)
> to establish that subsequent occurrences of the same form hold.

It's certainly true "in general", where predicate contents include functions 
with and depending on side-effects, where the initial state of objects is 
not defined, where privacy is not used properly. But why should we care 
about the optimization and performance of poorly designed software?

> Separately, even when reusing the same syntactic form of predicate in
> pre- and postconditions, optimizing out subsequent occurrences of the
> predicate may not be possible as often as one would hope.  Given two
> occurrences of the predicate P(X), to establish that the subsequent
> occurrence holds, it necessary (for the theorem above) to establish that
> the X is the same in both occurrences.  In the case that X is visible
> outside its package and between the two occurrences of P(X) there is
> a call to a subprogram in another package, I can't see how a compiler
> would know that X won't be changed.  (I'm assuming that compilers
> don't look at the bodies of other packages when compiling a package.)
> To avoid such issues, formal methods tools typically require
> subprograms to have a 'frame' annotation that indicates which variables
> a subprogram may change.

First of all, compilers do this all the time. Any compiler that takes 
advantage of 10.2.1(18/3) [and most do] have been doing this for many years. 
In addition, this is essentially the same problem as identifying common 
subexpressions, a problem that optimizers have been doing since the 
beginning of (computer) time. So there is absolutely nothing new here. (The 
only part of this that would be new in Janus/Ada is the idea of assumptions, 
and that fits in very well with our existing optimization technology.)

Secondly, one hopes that most that "predicates" are good, that is that they 
don't violate the Implementation Permission 11.4.2(27/3). One also hopes 
that most objects are of private types and are not modified "out-of-band" 
(whether this is possible is determinable from the declaration of the type, 
so it doesn't require looking into bodies to figure out - ignoring Chapter 
13 effects of course, which are usually erroneous if they have this sort of 
effect). And I'm assuming that function side-effects are declared somehow. 
(Without these things, you can't do any call optimizations without either 
looking in bodies or appealing to the Pure permissions of 10.2.1 - which are 
rarely applicable.)

I agree that Ada 2012 doesn't go far enough to define these things. The 
global in/global out contracts that we worked on but ended up abandoning as 
insufficiently fully baked certainly would have helped a lot.

We actually tried to come up with a rule for 11.4.2 that would have allowed 
such optimizations in all cases (that is certainly the intent -- that 
"assertions" that contain any sort of side-effects are bad). We didn't put 
it into the Standard because we weren't able to draft one that didn't throw 
out good things with the bad. But the intent is still there, and it's 
possible that such a rule (a version 10.2.1(18) for 11.4.2) will appear in 
the future.

>So, in summary, optimizing out predicates in pre- and postconditions may 
>not be that easy.

That's probably true in Ada 2012, especially if you don't use 
implementation-defined stuff like Pure_Function (in GNAT). That's why I was 
babbling about an Ada-like language with an extension to constraints that 
could carry the missing information. Perhaps there is a way to get that 
information into Ada as well (I'm not as sure).

                                                           Randy.

SPARK question

[Simon Wright]

With SPARK CE 2018, I'm seeing

   commander.ads:103:08: high: "memory accessed through objects of
   access type" must be a global Output of "Commander_Watchdog"

Google tells me nothing, any clues here? (and, obvs, where _should_ I be
asking?)

Re: SPARK question

[Shark8]

On Monday, August 27, 2018 at 8:10:13 AM UTC-6, Simon Wright wrote:
> With SPARK CE 2018, I'm seeing
> 
>    commander.ads:103:08: high: "memory accessed through objects of
>    access type" must be a global Output of "Commander_Watchdog"
> 
> Google tells me nothing, any clues here? (and, obvs, where _should_ I be
> asking?)

I think it's saying that you need a "Global" aspect on "Commander_Watchdog", see https://blog.adacore.com/spark-2014-rationale-data-dependencies -- in particular:

   procedure Add (X, Y : in Integer) with
     Global => (Output => Global_Variable);

Re: SPARK question

[Simon Wright]

Shark8 <onewingedshark@gmail.com> writes:

> On Monday, August 27, 2018 at 8:10:13 AM UTC-6, Simon Wright wrote:
>> With SPARK CE 2018, I'm seeing
>> 
>>    commander.ads:103:08: high: "memory accessed through objects of
>>    access type" must be a global Output of "Commander_Watchdog"
>> 
>> Google tells me nothing, any clues here? (and, obvs, where _should_ I be
>> asking?)
>
> I think it's saying that you need a "Global" aspect on
> "Commander_Watchdog", see
> https://blog.adacore.com/spark-2014-rationale-data-dependencies -- in
> particular:
>
>    procedure Add (X, Y : in Integer) with
>      Global => (Output => Global_Variable);

Yes, but! similar messages say e.g.

   commander.ads:103:08: high: "Current_System_Status" must be a global
   Output of "Commander_Watchdog"

and I can't see any "objects of access type" used in Commander_Watchdog.

Re: SPARK question

[Randy Brukardt]

"Simon Wright" <simon@pushface.org> wrote in message 
news:lyk1oblfz7.fsf@pushface.org...
> Shark8 <onewingedshark@gmail.com> writes:
>
>> On Monday, August 27, 2018 at 8:10:13 AM UTC-6, Simon Wright wrote:
>>> With SPARK CE 2018, I'm seeing
>>>
>>>    commander.ads:103:08: high: "memory accessed through objects of
>>>    access type" must be a global Output of "Commander_Watchdog"
>>>
>>> Google tells me nothing, any clues here? (and, obvs, where _should_ I be
>>> asking?)
>>
>> I think it's saying that you need a "Global" aspect on
>> "Commander_Watchdog", see
>> https://blog.adacore.com/spark-2014-rationale-data-dependencies -- in
>> particular:
>>
>>    procedure Add (X, Y : in Integer) with
>>      Global => (Output => Global_Variable);
>
> Yes, but! similar messages say e.g.
>
>   commander.ads:103:08: high: "Current_System_Status" must be a global
>   Output of "Commander_Watchdog"
>
> and I can't see any "objects of access type" used in Commander_Watchdog.

I'd guess that it comes from some dereference, and that might be in some 
subprogram that you called. (But I'm reasoning from the proposed Ada 2020 
rules and not the slightly different SPARK rules.) It's also possible that 
some Ada feature you used is internally implemented with an access type, but 
I wouldn't have expected SPARK to pick that up.

                                    Randy.

Re: SPARK question

[Simon Wright]

"Randy Brukardt" <randy@rrsoftware.com> writes:

> "Simon Wright" <simon@pushface.org> wrote in message 
> news:lyk1oblfz7.fsf@pushface.org...
>> Shark8 <onewingedshark@gmail.com> writes:
>>
>>> On Monday, August 27, 2018 at 8:10:13 AM UTC-6, Simon Wright wrote:
>>>> With SPARK CE 2018, I'm seeing
>>>>
>>>>    commander.ads:103:08: high: "memory accessed through objects of
>>>>    access type" must be a global Output of "Commander_Watchdog"
>>>>
>>>> Google tells me nothing, any clues here? (and, obvs, where _should_
>>>> I be asking?)
>>>
>>> I think it's saying that you need a "Global" aspect on
>>> "Commander_Watchdog", see
>>> https://blog.adacore.com/spark-2014-rationale-data-dependencies -- in
>>> particular:
>>>
>>>    procedure Add (X, Y : in Integer) with
>>>      Global => (Output => Global_Variable);
>>
>> Yes, but! similar messages say e.g.
>>
>>   commander.ads:103:08: high: "Current_System_Status" must be a global
>>   Output of "Commander_Watchdog"
>>
>> and I can't see any "objects of access type" used in
>> Commander_Watchdog.
>
> I'd guess that it comes from some dereference, and that might be in
> some subprogram that you called. (But I'm reasoning from the proposed
> Ada 2020 rules and not the slightly different SPARK rules.) It's also
> possible that some Ada feature you used is internally implemented with
> an access type, but I wouldn't have expected SPARK to pick that up.

I think you must be right. I had thought that gnatprove would choke on
any use of 'access', this is clearly not so (now).