Specifying preconditions

[Jörn Zaefferer]

Hi,

I'm currently trying out Reductio with a very simple Generator java
class. I'm testing a method that gets two arguments that have certain
preconditions.

My first attempt at this fails pretty quickly due to the second
argument violating its precondition (must be > 0 and > first
argument):

Property p = property(arbitrary(Gen.choose(1, 1000)),
arbitrary(Gen.choose(1, 1000)), new F2<Integer, Integer, Property>() {
public Property f(final Integer size, final Integer range) {
return prop(new Generator().generate(size, range).size() == size);
}
});

I then tried to put the precondition into the Property:

Property p = property(arbitrary(Gen.choose(1, 1000)),
arbitrary(Gen.choose(1, 5000)), new F2<Integer, Integer, Property>() {
public Property f(final Integer size, final Integer range) {
return bool(range > size).implies(new Generator().generate(size,
range).size() == size);
}
});

The problem here is that the generate method is still called with
invalid arguments, but that isn't allowed to happen. I tried to use
Gen.sized to replace Gen.choose, but can't figure out how to create a
tuple based on that.

Any ideas how to express those preconditions with Reductio?

Thanks
Jörn

[Ricky Clarkson]

Hi,

I guess you can do this in two ways, the second better than the first:

1. To ensure the second is always greater than the first, make the second be between 1001 and 5000 instead of between 1 and 5000.
2. As the generation of the second necessarily depends on the first, generate them together.  Something like:

Property p = property(arbitrary(new F0<Pair<Integer, Integer>>() {
 public Pair<Integer, Integer> f() {
  int a;
  return pair(a=random.nextInt(1000), a+1+random.nextInt(1000)); } },
 new F1<Integer, Property>() {
  public Property f(final Pair<Integer, Integer> sizeAndRange) {
   return prop(new Generator().generate(sizeAndRange._1, sizeAndRange._2).size() ==
    sizeAndRange.size()); } } );

2008/6/5 Jörn Zaefferer <joern.z...@googlemail.com>:

[Jörn Zaefferer]

Thanks for the answer Ricky. I can't get it working though: I don't
have an F0 interface on my classpath, nor Pair. Where do these come
from?

Implementing those myself shouldn't be necessary when using
Reductio...

Jörn

On Jun 5, 4:06 pm, "Ricky Clarkson" <ricky.clark...@gmail.com> wrote:
> Hi,
>
> I guess you can do this in two ways, the second better than the first:
>
> 1. To ensure the second is always greater than the first, make the second be
> between 1001 and 5000 instead of between 1 and 5000.
> 2. As the generation of the second necessarily depends on the first,
> generate them together. Something like:
>
> Property p = property(arbitrary(new F0<Pair<Integer, Integer>>() {
> public Pair<Integer, Integer> f() {
> int a;
> return pair(a=random.nextInt(1000), a+1+random.nextInt(1000)); } },
> new F1<Integer, Property>() {
> public Property f(final Pair<Integer, Integer> sizeAndRange) {
> return prop(new Generator().generate(sizeAndRange._1,
> sizeAndRange._2).size() ==
> sizeAndRange.size()); } } );
>

> 2008/6/5 Jörn Zaefferer <joern.zaeffe...@googlemail.com>:

[Ricky Clarkson]

I apologise.  I invented F0 and Pair and didn't look at what Reductio and Functional Java provide.  I could say I left that as an exercise for the reader, but really I was just being lazy and hoping you understood :)

Anyway, this is the first time I've used Reductio or Functional Java, so although this compiles and works fine, Tony probably has some things to say about it..

All it does is test that the second int is always bigger than the first though, so you'll have to adapt it to your case.

import static reductio.Arbitrary.arbitrary;
import reductio.Arbitrary;
import reductio.Gen;
import reductio.Rand;
import reductio.Property;
import static reductio.Property.prop;
import static reductio.Property.property;
import static reductio.CheckResult.summary;
import fj.F;
import static fj.P.p;
import fj.P2;

class Main {
 public static void main(String[] args) {
  Gen<P2<Integer, Integer>> gen = Gen.gen(new F<Integer, F<Rand, P2<Integer, Integer>>>() {
   public F<Rand, P2<Integer, Integer>> f(Integer num) { return new F<Rand, P2<Integer, Integer>>() {
    public P2<Integer, Integer> f(Rand rand) { int a;
                                               return p(a = rand.choose(1,1000), rand.choose(a + 1, a + 1000)); } }; } });
  Arbitrary<P2<Integer, Integer>> arb = arbitrary(gen);
  Property p = property(arb, new F<P2<Integer, Integer>, Property>() { public Property f(P2<Integer, Integer> pair) {
   return prop(pair._2() > pair._1()); } } );

  summary.println(p.check()); } }

2008/6/5 Jörn Zaefferer <joern.z...@googlemail.com>:

[Tony Morris]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hi Jörn,
I will answer your question in a general sense, since it may be
helpful for others in other settings; I hope you don't mind.

First, let's take a look at the truth table for logical implication:

p q p -> q
0 0 1
1 0 0
0 1 1
1 1 1

We see here that if p is false, then the value for the equation can be
determined without inspecting q (it's true!). This is a bit like &&
and || that are also lazy in their second argument. We want the same
for 'implies' so that the expression that is used for the value of 'q'
is not necessarily evaluated. Unfortunately, Java makes this a little
difficult, so you'll find two versions of the implies method. The one
you have used will evaluate both sides of the equation regardless but
is slightly easier to use.

Imagine a Java && that did this:
if(s != null && !s.isEmpty()) // ugh if s == null, we will get a NPE.

So, to actually answer your question; there is a version of 'implies'
that accepts a P1<Property> [1] and you can get a Property from a
boolean using the prop function [2]. (By the way, is Generator your
own type?)

return bool(range > size).implies(new P1<Property>() {
public Property _1() {

return prop(new Generator().generate(size, range).size() == size);
}
}

I hope this helps Jörn, but if not, please feel free to ask for more
clarification.

PS: I saw your comment on my blog, but Rickard beat me to answering :)

[1]
http://projects.workingmouse.com/public/reductio/artifacts/2.2//javadoc/reductio/Bool.html#implies(fj.P1)
[2]
http://projects.workingmouse.com/public/reductio/artifacts/2.2//javadoc/reductio/Property.html#prop(boolean)

- --
Tony Morris
http://tmorris.net/

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFISE9CmnpgrYe6r60RAtpJAKC5PhSrHZ5BYhZbh1mIEyX5HZu6NgCdFu1K
PLLNZx+bObGo/qvLortFpck=
=iaM8
-----END PGP SIGNATURE-----

[Tony Morris]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Ricky Clarkson wrote:
> I apologise. I invented F0 and Pair and didn't look at what
> Reductio and Functional Java provide. I could say I left that as an
> exercise for the reader, but really I was just being lazy and hoping
> you understood :)

Thanks Ricky for taking care of things while I was snoozing ;)

Functional Java provide fj.P1 and fj.P2 respectively for this scenario.

I'd also like add that Scala permits call-by-name function values, so
this problem does not pop up. Also, it allows non-alphanumeric method
names, so instead of 'implies' the method is called -> The scaladoc
for this function is here:

http://projects.workingmouse.com/public/reductio/artifacts/2.2//scaladoc/reductios/Bool.html#-%3E%28%3D%3Ereductio.Property%29

Note the annotation (=>) on the argument denoting its evaluation strategy.

You can see an example of the use of the -> method here:
http://reductiotest.org/examples/scala#IntegerOverflow

- --
Tony Morris
http://tmorris.net/

-----BEGIN PGP SIGNATURE-----

Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFISFN0mnpgrYe6r60RAiYQAKCK4vOAr0I4U/uG4GUCDakM5DZwBgCfakmz
WhVmaFc20dKMKKOi4zrFOPI=
=fZT1
-----END PGP SIGNATURE-----