* SPARK - runtime checks question
@ 2009-06-19 15:26 Maciej Sobczak
2009-06-19 15:31 ` Maciej Sobczak
` (2 more replies)
0 siblings, 3 replies; 8+ messages in thread
From: Maciej Sobczak @ 2009-06-19 15:26 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: SPARK - runtime checks question
2009-06-19 15:26 SPARK - runtime checks question Maciej Sobczak
@ 2009-06-19 15:31 ` Maciej Sobczak
2009-06-19 16:04 ` Rod Chapman
2009-06-19 18:33 ` Adam Beneschan
2 siblings, 0 replies; 8+ messages in thread
From: Maciej Sobczak @ 2009-06-19 15:31 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: SPARK - runtime checks question
2009-06-19 15:26 SPARK - runtime checks question Maciej Sobczak
2009-06-19 15:31 ` Maciej Sobczak
@ 2009-06-19 16:04 ` Rod Chapman
2009-06-19 18:29 ` Adam Beneschan
2009-06-19 21:38 ` Maciej Sobczak
2009-06-19 18:33 ` Adam Beneschan
2 siblings, 2 replies; 8+ messages in thread
From: Rod Chapman @ 2009-06-19 16:04 UTC (permalink / raw)
> 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.
^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: SPARK - runtime checks question
2009-06-19 16:04 ` Rod Chapman
@ 2009-06-19 18:29 ` Adam Beneschan
2009-06-19 18:55 ` Rod Chapman
2009-06-19 21:38 ` Maciej Sobczak
1 sibling, 1 reply; 8+ messages in thread
From: Adam Beneschan @ 2009-06-19 18:29 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: SPARK - runtime checks question
2009-06-19 15:26 SPARK - runtime checks question Maciej Sobczak
2009-06-19 15:31 ` Maciej Sobczak
2009-06-19 16:04 ` Rod Chapman
@ 2009-06-19 18:33 ` Adam Beneschan
2009-06-19 21:16 ` Maciej Sobczak
2 siblings, 1 reply; 8+ messages in thread
From: Adam Beneschan @ 2009-06-19 18:33 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: SPARK - runtime checks question
2009-06-19 18:29 ` Adam Beneschan
@ 2009-06-19 18:55 ` Rod Chapman
0 siblings, 0 replies; 8+ messages in thread
From: Rod Chapman @ 2009-06-19 18:55 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: SPARK - runtime checks question
2009-06-19 18:33 ` Adam Beneschan
@ 2009-06-19 21:16 ` Maciej Sobczak
0 siblings, 0 replies; 8+ messages in thread
From: Maciej Sobczak @ 2009-06-19 21:16 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: SPARK - runtime checks question
2009-06-19 16:04 ` Rod Chapman
2009-06-19 18:29 ` Adam Beneschan
@ 2009-06-19 21:38 ` Maciej Sobczak
1 sibling, 0 replies; 8+ messages in thread
From: Maciej Sobczak @ 2009-06-19 21:38 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 8+ messages in thread
end of thread, other threads:[~2009-06-19 21:38 UTC | newest]
Thread overview: 8+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2009-06-19 15:26 SPARK - runtime checks question Maciej Sobczak
2009-06-19 15:31 ` Maciej Sobczak
2009-06-19 16:04 ` Rod Chapman
2009-06-19 18:29 ` Adam Beneschan
2009-06-19 18:55 ` Rod Chapman
2009-06-19 21:38 ` Maciej Sobczak
2009-06-19 18:33 ` Adam Beneschan
2009-06-19 21:16 ` Maciej Sobczak
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox