[<Property(Arbitrary=[| typeof<ArbitraryModifiers> |])>]OUTPUT:
let ``Closed under multiplication`` (y : WholeNumber) (z : WholeNumber) =
(WholeNumber.get y) * (WholeNumber.get z) >= 0
Test.Geometry.Closed under multiplication [FAIL]
Falsifiable, after 3 tests (0 shrinks) (StdGen (603380185,295587877)):
(WholeNumber 13118, WholeNumber 227510903)
In other words, the system is able to automatically prove that whole numbers (implemented on top of .NET Int32) are not, in fact, closed under multiplication because of integer overflow, since 13118 * 227510903 = -514245166.
Then, I change WholeNumber so that it is built on top of bigint (arbitrary-sized integers as in math, not computer architecture) and alter the test slightly to use 0I (bigint version of zero).
Then, I change WholeNumber so that it is built on top of bigint (arbitrary-sized integers as in math, not computer architecture) and alter the test slightly to use 0I (bigint version of zero).
[<Property(Arbitrary=[| typeof<ArbitraryModifiers> |])>]
let ``Closed under multiplication`` (y : WholeNumber) (z : WholeNumber) =
(WholeNumber.get y) * (WholeNumber.get z) >= 0I
OUTPUT:
Tests complete: 1 of 3Tests complete: 2 of 3Tests complete: 3 of 33 total, 0 failed, 0 skipped, took 1.790 seconds
Voila! My program now matches my spec.
-Max
Hahahahaaaa!!! That is ME laughing at YOU, cruel world.
-Jordan Rixon
I could not love thee, dear, so much,
Loved I not Honour more.
No comments:
Post a Comment