Improve "How to Specify it! In Java"

[jlink]

Please add any comments and suggestions to this issue. Thank you all!

[gtrefs]

I did not yet read all of it but I really like this "translation". I did not read the oroginal, yet.

In section 4.2 you forgot to replace k with key and k' with otherKey in the paragraph.

[jlink]

@gtrefs Thanks. Fixed.

[gtrefs]

Maybe a little explanation what integrated shrinking is would help. Is there a way to explain it in 3 or 4 sentences?

[gtrefs]

I found a t here: Informally, we expect the effect of inserting key1 value1 into t before calling. Should be tree.

[jlink]

@gtrefs

In general, jqwik supports integrated shrinking which ensures that all preconditions used during data generation will also be preserved while shrinking. In addition shrinkers are directly derived from generators and must not be implemented separately.

Will that do?

[gtrefs]

In 4.6:

@Property(tries = 1_000_000)
void measure(
        @ForAll Integer key,
        @ForAll("trees") BST<Integer, Integer> bst
) {
    List<Integer> keys = bst.keys();
    
    String frequency = keys.contains(key) ? "present" : "absent";
    Statistics.label("frequency").collect(frequency);

    String position =
            bst.isLeaf() ? "empty"
            : keys.equals(Collections.singletonList(key)) ? "just key"
            : keys.get(0).equals(key) ? "at start"
            : keys.get(keys.size() - 1 ).equals(key) ? "at end"
            : "middle";
    Statistics.label("position").collect(position);
}

When I follow this explanation:

[BST Properties:measure] frequency = 
    absent  : 89 %
    present : 11 %

[BST Properties:measure] position = 
    middle   : 98.18 %
    empty    : 1.36 %
    at end   : 0.24 %
    at start : 0.21 %
    just key : 0.0 %

From the second table, we can see that key appears at the beginning or end of the keys in bst about 10% 0.5% of the time for each case, while it appears somewhere in the middle of the sequences of keys 75% 98% of the time. This looks quite reasonable. On the other hand, in almost 80% 90% of tests, key is not found in the tree at all!

I assume that the statistics in the second table is about the position of the key in the tree when it is present in the tree. The code tells a different story. When the key is not in the tree, it is counted as middle. I had a look at the original paper and there it is done in the same way. Am I mistaken?

[jlink]

Here's the original:

prop Measure k t =
    label (if k ∈ keys t then "present" else "absent") $ 
    label (if t ≡ nil then "empty" else
        if keys t ≡ [k] then "just k" else
        if (all (>= k) (keys t)) then "at start" else 
        if (all (<= k) (keys t)) then "at end" else "middle") $
True

I'd say that this code will label k's position regardless of it being present in t (<= and >= work even if k is not in t). But you are right about my code being wrong since classification only works if key is in bst.

[jlink]

Here's the adapted statistics code:

String position =
  bst.isLeaf() ? "empty" :
    keys.equals(Collections.singletonList(key)) ? "just key" :
    keys.stream().allMatch(k -> k.compareTo(key) >= 0) ? "at start" :
    keys.stream().allMatch(k -> k.compareTo(key) <= 0) ? "at end" : "middle";
Statistics.label("position").collect(position);

This seems to better reflect the original code. And the results are indeed closer to the QuickCheck results:

[BST Properties:measure] position = 
    middle   : 94.03 %
    at start : 2.29 %
    at end   : 2.29 %
    empty    : 1.39 %
    just key : 0.0 %