deletion challenge

[kostis]

The deletion challenge as well as its original source are sub-optimal (as PBT challenges) in my opinion -- at least the way they are currently implemented.

Given a list delete implementation that removes only the first occurrence of the element that is to be removed, instead of testing for the property:

• "if we remove an element from a list, the element is no longer in the list"

the challenge for PBT tools should be testing the following more general property instead:

• "if we remove an integer from a list of integers, the integer is no longer present in the list".

The difference in what a PBT tool needs to do, both in generation and shrinking, is significant.

1. For starters, it's quite challenging to generate both a random integer x and a list of integers that contains x at least twice in order to falsify this property. So, this tests the effectiveness of the generation component.

2. When a counterexample is found, the two (independent) generators have to be shrunk in concert.

I propose to update the challenge to this one.

[jlink]

I'd be happy to change the challenge in that way.

@DRMacIver What do you think?

[DRMacIver]

I don't mind the change, certainly, but I think it might need a bit of clarification. Specifying "list of integers" is uncontroversial and I agree it's a good change, but I don't think it's clear enough from the proposed change that the removed integer should be generated fully independently from the list, which I think is the intent? Maybe adding something like "The element to be deleted should be generated without reference to the generated list." as well?

[kostis]

... I don't think it's clear enough from the proposed change that the removed integer should be generated fully independently from the list, which I think is the intent?

Yes, that's the intent.

I am fine with whatever phrasing makes this intent as clear as it can get.

[jlink]

1. For starters, it's quite challenging to generate _both_ a random integer **x** and a list of integers that contains **x** at 
   least twice in order to falsify this property.  So, this tests the effectiveness of the generation component.

I'm not quite sure of that one. Do you think that given two random and independent generators,

• one to generate an unconstrained integer (32bits) and
• one to generate an unconstrained list of integers,
  the probability to have the independently generated integer in the list twice should be high enough to be usually hit in a single run of the property?

If I - as the property writer - had an inkling that the individual integer is somehow connected to the list I'd definitely tune the generator in that direction or at least check statistically that it occurs regularly in the list. If I do not have that inkling why should a generator prioritize duplication of that exact constellation?