* Preconditions which anyway would be caught? @ 2014-08-09 15:35 Victor Porton 2014-08-09 15:40 ` mockturtle ` (2 more replies) 0 siblings, 3 replies; 11+ messages in thread From: Victor Porton @ 2014-08-09 15:35 UTC (permalink / raw) function Inverse (X: Float) is begin return 1/X; end with Pre => (X /= 0); Is this precondition superfluous? (it anyway could be caught by erroneous 1/X operation) -- Victor Porton - http://portonvictor.org ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Preconditions which anyway would be caught? 2014-08-09 15:35 Preconditions which anyway would be caught? Victor Porton @ 2014-08-09 15:40 ` mockturtle 2014-08-09 16:08 ` Jeffrey Carter 2014-08-09 19:21 ` Peter Chapin 2 siblings, 0 replies; 11+ messages in thread From: mockturtle @ 2014-08-09 15:40 UTC (permalink / raw) On Saturday, August 9, 2014 5:35:21 PM UTC+2, Victor Porton wrote: > function Inverse (X: Float) is > > begin > return 1/X; > end > with Pre => (X /= 0); > > Is this precondition superfluous? (it anyway could be caught by erroneous > 1/X operation) Still not a LL... I would say it is not. It depends on the "reason" for specifying the precondition. As I see it, the precondition is a kind of "formal documentation" of the conditions that must be satisfied when you call the function. As a side effect, you can have those conditions checked at run-time as a "bug trap," but, for example, they could be used by some formal checking software. So, even if calling the function with X=0 will cause an error, I would keep the precondition. Riccardo ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Preconditions which anyway would be caught? 2014-08-09 15:35 Preconditions which anyway would be caught? Victor Porton 2014-08-09 15:40 ` mockturtle @ 2014-08-09 16:08 ` Jeffrey Carter 2014-08-09 19:21 ` Peter Chapin 2 siblings, 0 replies; 11+ messages in thread From: Jeffrey Carter @ 2014-08-09 16:08 UTC (permalink / raw) On 08/09/2014 08:35 AM, Victor Porton wrote: > function Inverse (X: Float) is > begin > return 1/X; > end > with Pre => (X /= 0); > > Is this precondition superfluous? (it anyway could be caught by erroneous > 1/X operation) This won't compile, so you have no problem. Considering your general question, there are a number of differences between the 2: Preconditions serve an important documentation purpose, which simply having an error caught at run time doesn't fulfill. Preconditions can be used by tools, which might not be able to use the run-time check on division. The precondition adds a check to every call of the function, and the division is not performed if the precondition fails. The division, and any associated check, is always performed without the precondition. An alternative might be to use a subtype subtype Invertable_Float is Float with Dynamic_Predicate => Invertible_Float /= 0.0; function Invert (X : Invertable_Float) return Float; Finally, are you sure the division will raise an exception? with Ada.Command_Line; with Ada.Text_IO; procedure Inverse_Test is function Inverse (X : Float) return Float is -- Empty declarative part begin -- Inverse return 1.0 / X; end Inverse; F : constant Float := Inverse (Float'Value (Ada.Command_Line.Argument (1) ) ); begin -- Inverse_Test Ada.Text_IO.Put_Line (Item => Float'Image (F) ); end Inverse_Test; $ gnatmake -gnatano -fstack-check -gnatwa inverse_test.adb gcc-4.6 -c -gnatano -fstack-check -gnatwa inverse_test.adb gnatbind -x inverse_test.ali gnatlink inverse_test.ali -fstack-check $ ./inverse_test 0.0 +Inf******* You might want to review floating-point types and look at the 'Machine_Overflows attribute. -- Jeff Carter "Insufficient laughter--that's grounds for divorce." Play It Again, Sam 126 ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Preconditions which anyway would be caught? 2014-08-09 15:35 Preconditions which anyway would be caught? Victor Porton 2014-08-09 15:40 ` mockturtle 2014-08-09 16:08 ` Jeffrey Carter @ 2014-08-09 19:21 ` Peter Chapin 2014-08-09 19:24 ` Peter Chapin 2 siblings, 1 reply; 11+ messages in thread From: Peter Chapin @ 2014-08-09 19:21 UTC (permalink / raw) On 2014-08-09 11:35, Victor Porton wrote: > function Inverse (X: Float) is > begin > return 1/X; > end > with Pre => (X /= 0); > > Is this precondition superfluous? (it anyway could be caught by erroneous > 1/X operation) Proper syntax here is function Inverse(X : Float) with Pre => (X /= 0) is begin return 1/X; end; SPARK 2014 will attempt to prove that the precondition is satisfied at every call site. It will also try to prove that 1/X will never entail division by zero, which is trivial to do with the precondition present. If you remove the precondition, SPARK will not try to prove anything about X at the call site but it will still try to prove that 1/X does not entail division by zero. Unfortunately there isn't enough information to make that second proof go through so you'll end up with an undischarged verification condition. The precondition is a statement about the intended behavior of the subprogram. It is, in some sense, part of the subprogram's design. Without the precondition you are implying that it is okay to call Inverse for any Float value at all. What is the subprogram supposed to do when given 0.0? Raising Constraint_Error is unsightly because it typically means the programmer made a mistake. So the version without the precondition might more correctly be written as function Inverse(X : Float) is begin if X = 0.0. then raise Invalid_Domain; -- Documented exception for this purpose. else return 1/X; end if; end; Peter ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Preconditions which anyway would be caught? 2014-08-09 19:21 ` Peter Chapin @ 2014-08-09 19:24 ` Peter Chapin 2014-08-09 21:04 ` Niklas Holsti 0 siblings, 1 reply; 11+ messages in thread From: Peter Chapin @ 2014-08-09 19:24 UTC (permalink / raw) On 2014-08-09 15:21, Peter Chapin wrote: > Proper syntax here is > > function Inverse(X : Float) > with Pre => (X /= 0) is > begin > return 1/X; > end; Well that's closer. How about function Inverse(X : Float) return Float with Pre => (X /=0) is begin return 1/X; end; Peter ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Preconditions which anyway would be caught? 2014-08-09 19:24 ` Peter Chapin @ 2014-08-09 21:04 ` Niklas Holsti 2014-08-09 22:57 ` Peter Chapin 2014-08-10 7:24 ` Dmitry A. Kazakov 0 siblings, 2 replies; 11+ messages in thread From: Niklas Holsti @ 2014-08-09 21:04 UTC (permalink / raw) On 14-08-09 22:24 , Peter Chapin wrote: > On 2014-08-09 15:21, Peter Chapin wrote: > >> Proper syntax here is >> >> function Inverse(X : Float) >> with Pre => (X /= 0) is >> begin >> return 1/X; >> end; > > Well that's closer. How about > > function Inverse(X : Float) return Float > with Pre => (X /=0) is > begin > return 1/X; > end; Just to be a pedant: shouldn't that have some decimals on the literals: function Inverse(X : Float) return Float with Pre => (X /= 0.0) is begin return 1.0/X; end; In addition, is it really true that all Float numbers /= 0.0 can be inverted without error? What if X is a denormalized number which has suffered gradual underflow... won't its inverse overflow, because there is no concept of "gradual overflow" in IEEE floats? -- Niklas Holsti Tidorum Ltd niklas holsti tidorum fi . @ . ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Preconditions which anyway would be caught? 2014-08-09 21:04 ` Niklas Holsti @ 2014-08-09 22:57 ` Peter Chapin 2014-08-10 20:58 ` Niklas Holsti 2014-08-10 7:24 ` Dmitry A. Kazakov 1 sibling, 1 reply; 11+ messages in thread From: Peter Chapin @ 2014-08-09 22:57 UTC (permalink / raw) On 2014-08-09 17:04, Niklas Holsti wrote: > Just to be a pedant: shouldn't that have some decimals on the literals: > > function Inverse(X : Float) return Float > with Pre => (X /= 0.0) is > begin > return 1.0/X; > end; > > In addition, is it really true that all Float numbers /= 0.0 can be > inverted without error? What if X is a denormalized number which has > suffered gradual underflow... won't its inverse overflow, because there > is no concept of "gradual overflow" in IEEE floats? I wondered about that also, in fact. I just tried it with your corrections so it actually *does* compile. Without any precondition SPARK 2014 complains that overflow check might fail divide by zero check might fail With the precondition of X /= 0.0 SPARK says overflow check might fail However, this proves fine: function Inverse(X : Float) return Float with Pre => not(-1.0E-35 < X and X < +1.0E-35) is begin return 1.0/X; end; I didn't experiment to see how close to zero I could make the bounds in the precondition but clearly your concern is a valid one. Peter ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Preconditions which anyway would be caught? 2014-08-09 22:57 ` Peter Chapin @ 2014-08-10 20:58 ` Niklas Holsti 0 siblings, 0 replies; 11+ messages in thread From: Niklas Holsti @ 2014-08-10 20:58 UTC (permalink / raw) On 14-08-10 01:57 , Peter Chapin wrote: > On 2014-08-09 17:04, Niklas Holsti wrote: > >> Just to be a pedant: shouldn't that have some decimals on the literals: >> >> function Inverse(X : Float) return Float >> with Pre => (X /= 0.0) is >> begin >> return 1.0/X; >> end; >> >> In addition, is it really true that all Float numbers /= 0.0 can be >> inverted without error? What if X is a denormalized number which has >> suffered gradual underflow... won't its inverse overflow, because there >> is no concept of "gradual overflow" in IEEE floats? > > I wondered about that also, in fact. > > I just tried it with your corrections so it actually *does* compile. > Without any precondition SPARK 2014 complains that > > overflow check might fail > divide by zero check might fail > > With the precondition of X /= 0.0 SPARK says > > overflow check might fail > > However, this proves fine: > > function Inverse(X : Float) return Float > with Pre => not(-1.0E-35 < X and X < +1.0E-35) is > begin > return 1.0/X; > end; > > I didn't experiment to see how close to zero I could make the bounds in > the precondition but clearly your concern is a valid one. I think the actual precondition and function were only examples to illustrate the OP's question, so we are off-topic, too bad. But to continue: I wrote a program that initializes X to 1.0 and repeatedly divides by 2.0 until X is zero, printing X and 1.0/X each time. The break is here: X = 1.17549E-38, 1.0/X = 8.50706E+37 X = 5.87747E-39, 1.0/X = 1.70141E+38 X = 2.93874E-39, 1.0/X = +Inf******* X = 1.46937E-39, 1.0/X = +Inf******* and the last non-zero value is X = 1.40130E-45, 1.0/X = +Inf******* This is with an unconstrained X : Float. Float'Machine_Overflows is False. If I assign 1.0 / X to a variable Y of the subtype "Float range Float'Range" I of course get a Constraint_Error instead of the +Inf. Computing 1.0 / Float'Last gives 2.93874E-39, and a compile-time (!) warning from GNAT that "gradual underflow causes loss of precision". Neat. -- Niklas Holsti Tidorum Ltd niklas holsti tidorum fi . @ . ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Preconditions which anyway would be caught? 2014-08-09 21:04 ` Niklas Holsti 2014-08-09 22:57 ` Peter Chapin @ 2014-08-10 7:24 ` Dmitry A. Kazakov 2014-08-11 0:00 ` Shark8 1 sibling, 1 reply; 11+ messages in thread From: Dmitry A. Kazakov @ 2014-08-10 7:24 UTC (permalink / raw) On Sun, 10 Aug 2014 00:04:11 +0300, Niklas Holsti wrote: > On 14-08-09 22:24 , Peter Chapin wrote: >> On 2014-08-09 15:21, Peter Chapin wrote: >> >>> Proper syntax here is >>> >>> function Inverse(X : Float) >>> with Pre => (X /= 0) is >>> begin >>> return 1/X; >>> end; >> >> Well that's closer. How about >> >> function Inverse(X : Float) return Float >> with Pre => (X /=0) is >> begin >> return 1/X; >> end; > > Just to be a pedant: shouldn't that have some decimals on the literals: > > function Inverse(X : Float) return Float > with Pre => (X /= 0.0) is > begin > return 1.0/X; > end; > > In addition, is it really true that all Float numbers /= 0.0 can be > inverted without error? What if X is a denormalized number which has > suffered gradual underflow... won't its inverse overflow, because there > is no concept of "gradual overflow" in IEEE floats? But 1.0/0.0 is perfectly OK in IEEE floats. It is NaN. Methodically the approach is wrong. A precondition is chosen to ensure the post-condition. What is the post-condition of Inverse? 1. Whatever garbage but no exceptions 2. 1.0/X * X in 1.0 - err .. 1.0 + err ... Once the post-condition is defined, the precondition is the least constraint allowing an implementation that ensures it. Specifying precondition for the sake of having them is meaningless. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Preconditions which anyway would be caught? 2014-08-10 7:24 ` Dmitry A. Kazakov @ 2014-08-11 0:00 ` Shark8 2014-08-11 7:31 ` Dmitry A. Kazakov 0 siblings, 1 reply; 11+ messages in thread From: Shark8 @ 2014-08-11 0:00 UTC (permalink / raw) On 10-Aug-14 01:24, Dmitry A. Kazakov wrote: > Specifying precondition for the sake of having them is meaningless. Not all preconditions imply a post-condition; sometimes it's simply to constrain the values that you're willing to entertain; for example if you have Natural_Float being a subtype of float (range 0.0 .. Float'Last) you could use this in an internal simple simulator with Square_Root(X: Natural_Float) return Float being a function therein. ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Preconditions which anyway would be caught? 2014-08-11 0:00 ` Shark8 @ 2014-08-11 7:31 ` Dmitry A. Kazakov 0 siblings, 0 replies; 11+ messages in thread From: Dmitry A. Kazakov @ 2014-08-11 7:31 UTC (permalink / raw) On Sun, 10 Aug 2014 18:00:36 -0600, Shark8 wrote: > On 10-Aug-14 01:24, Dmitry A. Kazakov wrote: >> Specifying precondition for the sake of having them is meaningless. > > Not all preconditions imply a post-condition; sometimes it's simply to > constrain the values that you're willing to entertain; All. > for example if > you have Natural_Float being a subtype of float (range 0.0 .. > Float'Last) you could use this in an internal simple simulator with > Square_Root(X: Natural_Float) return Float being a function therein. The precondition of Square_Root en-force is True, thus calling Square_Root (-1.0) is not an error. Constraints are "dynamic preconditions" in Ada 2012 Newspeak. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 11+ messages in thread
end of thread, other threads:[~2014-08-11 7:31 UTC | newest] Thread overview: 11+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2014-08-09 15:35 Preconditions which anyway would be caught? Victor Porton 2014-08-09 15:40 ` mockturtle 2014-08-09 16:08 ` Jeffrey Carter 2014-08-09 19:21 ` Peter Chapin 2014-08-09 19:24 ` Peter Chapin 2014-08-09 21:04 ` Niklas Holsti 2014-08-09 22:57 ` Peter Chapin 2014-08-10 20:58 ` Niklas Holsti 2014-08-10 7:24 ` Dmitry A. Kazakov 2014-08-11 0:00 ` Shark8 2014-08-11 7:31 ` Dmitry A. Kazakov
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox