* SPARK - division by zero problem
@ 2013-04-18 8:14 Maciej Sobczak
2013-04-18 8:35 ` Phil Thornley
0 siblings, 1 reply; 3+ messages in thread
From: Maciej Sobczak @ 2013-04-18 8:14 UTC (permalink / raw)
While playing with SPARK (I also agree that comp.lang.ada is adequate for SPARK content) I have found a problem that can be shown in the following stripped-down example:
<my_package.ads>
package My_Package is
procedure Divide (X : in Integer; Y : in Integer; Z : out Integer);
--# derives Z from X, Y;
--# pre Y /= 0;
--# post Z = X / Y;
end My_Package;
<my_package.adb>
package body My_Package is
procedure Divide (X : in Integer; Y : in Integer; Z : out Integer) is
begin
Z := X / Y; -- this is line 5
end Divide;
end My_Package;
In this example I would expect the VC associated with rtc on line 5 above to be discharged based on the hypothesis from Divide's precondition: that is, Y is known to be non-zero, so division by zero in line 5 cannot happen.
Tools are invoked in the following order:
$ sparkmake
$ spark -index_file=spark.idx -vcg -config_file=config.cfg -output_dir=spark my_package.adb
$ sparksimp
$ pogs
The summary says that the VC in question in undischarged.
Is there anything missing?
The tools come from Ubuntu packages and announce themselves as GPL 2011.
--
Maciej Sobczak * http://www.msobczak.com * http://www.inspirel.com
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: SPARK - division by zero problem
2013-04-18 8:14 SPARK - division by zero problem Maciej Sobczak
@ 2013-04-18 8:35 ` Phil Thornley
2013-04-18 10:28 ` Maciej Sobczak
0 siblings, 1 reply; 3+ messages in thread
From: Phil Thornley @ 2013-04-18 8:35 UTC (permalink / raw)
In article <0dbac307-0c0c-4883-8644-d1ffc25419f8@googlegroups.com>,
see.my.homepage@gmail.com says...
>
> While playing with SPARK (I also agree that comp.lang.ada is adequate for SPARK content) I have found a problem that can be shown in the following stripped-down example:
>
> <my_package.ads>
> package My_Package is
>
> procedure Divide (X : in Integer; Y : in Integer; Z : out Integer);
> --# derives Z from X, Y;
> --# pre Y /= 0;
> --# post Z = X / Y;
>
> end My_Package;
>
> <my_package.adb>
> package body My_Package is
>
> procedure Divide (X : in Integer; Y : in Integer; Z : out Integer) is
> begin
> Z := X / Y; -- this is line 5
> end Divide;
>
> end My_Package;
>
> In this example I would expect the VC associated with rtc on line 5 above to be discharged based on the hypothesis from Divide's precondition: that is, Y is known to be non-zero, so division by zero in line 5 cannot happen.
>
> Tools are invoked in the following order:
>
> $ sparkmake
> $ spark -index_file=spark.idx -vcg -config_file=config.cfg -output_dir=spark my_package.adb
> $ sparksimp
> $ pogs
>
> The summary says that the VC in question in undischarged.
> Is there anything missing?
>
> The tools come from Ubuntu packages and announce themselves as GPL 2011.
The undischarged VC I get is:
procedure_divide_1.
H1: y <> 0 .
H2: x >= - 2147483648 .
H3: x <= 2147483647 .
H4: y >= - 2147483648 .
H5: y <= 2147483647 .
H6: integer__size >= 0 .
->
C1: x div y <= 2147483647 .
which is false for x = -2147483648, y = -1
Cheers,
Phil
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: SPARK - division by zero problem
2013-04-18 8:35 ` Phil Thornley
@ 2013-04-18 10:28 ` Maciej Sobczak
0 siblings, 0 replies; 3+ messages in thread
From: Maciej Sobczak @ 2013-04-18 10:28 UTC (permalink / raw)
Cc: phil.jpthornley
W dniu czwartek, 18 kwietnia 2013 10:35:48 UTC+2 użytkownik Phil Thornley napisał:
> The undischarged VC I get is:
> procedure_divide_1.
> H1: y <> 0 .
> H2: x >= - 2147483648 .
> H3: x <= 2147483647 .
> H4: y >= - 2147483648 .
> H5: y <= 2147483647 .
> H6: integer__size >= 0 .
> ->
> C1: x div y <= 2147483647 .
>
> which is false for x = -2147483648, y = -1
Right, I fell into the trap by focusing on Y /= 0 condition. Indeed, the assymetry of Integer'Range is causing troubles in this case.
Thank you for response.
--
Maciej Sobczak * http://www.msobczak.com * http://www.inspirel.com
^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2013-04-18 10:28 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2013-04-18 8:14 SPARK - division by zero problem Maciej Sobczak
2013-04-18 8:35 ` Phil Thornley
2013-04-18 10:28 ` Maciej Sobczak
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox