SPARK - runtime checks question

SPARK - runtime checks question

[Maciej Sobczak]

Consider the following:

-- my_package.ads:
package My_Package is
   function Distance (X : in Natural; Y : in Natural) return Natural;
end My_Package;

-- my_package.adb:
package body My_Package is

   function Distance (X : in Natural; Y : in Natural) return Natural
   is
      Result : Natural;
   begin
      if X > Y then
         Result := X - Y;    // line 8
      else
         Result := Y - X;    // line 10
      end if;
      return Result;
   end Distance;

end My_Package;

The Distance function is supposed to compute the distance between two
Naturals.

I have a problem with rtc checks that are generated for line 8 and 10.
After running spark -vcg, sparksimp and pogs, the spark.sum file
contains this:

VCs for function_distance :
----------------------------------------------------------------------------
      |       |                     |  -----Proved In-----  |
|       |
 #    | From  | To                  | vcg | siv | plg | prv | False |
TO DO |
----------------------------------------------------------------------------
 1    | start | rtc check @ 8       |     |     |     |     |       |
YES  |
 2    | start | rtc check @ 10      |     |     |     |     |       |
YES  |
 3    | start |    assert @ finish  |     | YES |     |     |
|       |
 4    | start |    assert @ finish  |     | YES |     |     |
|       |
----------------------------------------------------------------------------

and of course 50% of VCs are undischarged in the final report.

As far as I understand the math, the relevant values are always within
the target type. What am I missing in this simple example?

--
Maciej Sobczak * www.msobczak.com * www.inspirel.com

Database Access Library for Ada: www.inspirel.com/soci-ada

Re: SPARK - runtime checks question

[Maciej Sobczak]

On 19 Cze, 17:26, Maciej Sobczak <see.my.homep...@gmail.com> wrote:

>          Result := X - Y;    // line 8
>       else
>          Result := Y - X;    // line 10

Oops - as you can imagine, these strange foreign-looking comments were
added later on. :-)

--
Maciej Sobczak * www.msobczak.com * www.inspirel.com

Database Access Library for Ada: www.inspirel.com/soci-ada

Re: SPARK - runtime checks question

[Rod Chapman]

> and of course 50% of VCs are undischarged in the final report.

The Examiner, by default, doesn't know the values of Natural'First
and Natural'Last, since these are implementation-defined.

You can supply these values with a configuration file - see
the Examiner User Manual.  Run the Examiner
with the -conf switch to re-generate the VCs, then re-simplify.
I then get 100% of the VCs proved.
 - Rod Chapman, SPARK Team

PS...we now always recommend the use of -vcg not -rtc
to generate VCs now.

Re: SPARK - runtime checks question

[Adam Beneschan]

On Jun 19, 9:04 am, Rod Chapman <roderick.chap...@googlemail.com>
wrote:
> > and of course 50% of VCs are undischarged in the final report.
>
> The Examiner, by default, doesn't know the values of Natural'First
> and Natural'Last, since these are implementation-defined.

Ummm... only half right.  If Natural'First is implementation-defined,
you're working with a rather bizarre implementation.

                           -- Adam

Re: SPARK - runtime checks question

[Adam Beneschan]

On Jun 19, 8:26 am, Maciej Sobczak <see.my.homep...@gmail.com> wrote:
> Consider the following:
>
> -- my_package.ads:
> package My_Package is
>    function Distance (X : in Natural; Y : in Natural) return Natural;
> end My_Package;
>
> -- my_package.adb:
> package body My_Package is
>
>    function Distance (X : in Natural; Y : in Natural) return Natural
>    is
>       Result : Natural;
>    begin
>       if X > Y then
>          Result := X - Y;    // line 8
>       else
>          Result := Y - X;    // line 10
>       end if;
>       return Result;
>    end Distance;
>
> end My_Package;

Apologies in advance for answering a question you didn't ask, but...
any reason not to simply return abs(X-Y)?  If you're thinking that the
result of X-Y will raise a Constraint_Error if it's negative---it
won't.  (At least not in Ada.  I don't know much about SPARK---it
wouldn't raise Constraint_Error there either, would it?)

                                -- Adam

Re: SPARK - runtime checks question

[Rod Chapman]

On Jun 19, 7:29 pm, Adam Beneschan <a...@irvine.com> wrote:
> Ummm... only half right.  If Natural'First is implementation-defined,
> you're working with a rather bizarre implementation.

Doh!  I'll go straight to the back of the class then... :-)
  - Rod

Re: SPARK - runtime checks question

[Maciej Sobczak]

On 19 Cze, 20:33, Adam Beneschan <a...@irvine.com> wrote:

> Apologies in advance for answering a question you didn't ask, but...
> any reason not to simply return abs(X-Y)?

Sure. This example was a minimal version of the problem which I have
found while fooling around with some other algorithm. I did not want
to complicate the discussion and posted the smallest function that
still exhibits the same issue and also makes sense in isolation.

--
Maciej Sobczak * www.msobczak.com * www.inspirel.com

Database Access Library for Ada: www.inspirel.com/soci-ada

Re: SPARK - runtime checks question

[Maciej Sobczak]

On 19 Cze, 18:04, Rod Chapman <roderick.chap...@googlemail.com> wrote:

> The Examiner, by default, doesn't know the values of Natural'First
> and Natural'Last, since these are implementation-defined.
>
> You can supply these values with a configuration file - see
> the Examiner User Manual.  Run the Examiner
> with the -conf switch to re-generate the VCs, then re-simplify.
> I then get 100% of the VCs proved.

Done, it works - thank you. I have used the confgen program form lib/
spark.

Is it considered to be a good practice to always provide the config
file that was generated for the target platform?

BTW - when the config file is provided, spark always reports this:

           Reading target configuration file ...

  10     type Address is private;

---        Note              :  3: The deferred constant Null_Address
has been
           implicitly defined here.

  21     subtype Priority is Any_Priority range  0 ..  62;

---        Note              :  4: The constant Default_Priority, of
type Priority,
           has been implicitly defined here.

[...]

    2 errors or warnings, comprising:
         2 warnings

Is this normal?

--
Maciej Sobczak * www.msobczak.com * www.inspirel.com

Database Access Library for Ada: www.inspirel.com/soci-ada