From: Maciej Sobczak <see.my.homepage@gmail.com>
Subject: SPARK - division by zero problem
Date: Thu, 18 Apr 2013 01:14:06 -0700 (PDT)
Date: 2013-04-18T01:14:06-07:00 [thread overview]
Message-ID: <0dbac307-0c0c-4883-8644-d1ffc25419f8@googlegroups.com> (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
next reply other threads:[~2013-04-18 8:14 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2013-04-18 8:14 Maciej Sobczak [this message]
2013-04-18 8:35 ` SPARK - division by zero problem Phil Thornley
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