From: Phil Thornley <phil.jpthornley@gmail.com>
Subject: Re: SPARK - division by zero problem
Date: Thu, 18 Apr 2013 09:35:48 +0100
Date: 2013-04-18T09:35:48+01:00 [thread overview]
Message-ID: <MPG.2bd9c09a49da8ab39896a4@news.zen.co.uk> (raw)
In-Reply-To: 0dbac307-0c0c-4883-8644-d1ffc25419f8@googlegroups.com
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
next prev parent reply other threads:[~2013-04-18 8:35 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2013-04-18 8:14 SPARK - division by zero problem Maciej Sobczak
2013-04-18 8:35 ` Phil Thornley [this message]
2013-04-18 10:28 ` Maciej Sobczak
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox