One starts by writing a parameterized unit test that translates Test 1 in C#. Notice that, each time 'for any' is used in the test description a parameter is added to the test method:

[TestClass, PexClass]
public partial class ChunkerTest 
{
    [PexTest]
    public void Chunk(string value, int length) 
    {
        Chunker chunker = new Chunker(value, length);
        string result = null;
        for (string chunk = chunker.Next();
            chunk != null;
            chunk = chunker.Next())
            result += chunk;
        Assert.AreEqual(value, result);
    }
}

A minimal implementation of Chunker is written to have the code compile.

public class Chunker {
    public Chunker(string value, int length) { }
    internal string Next() 
    {
        return null;
    }
}

Using the Visual Studio integration, Pex is invoked and starts exploring the test. Pex generates 2 unit test cases, one that passes null and succeeds, one that passes the empty string and fails. This was found by a systematic exploration of the program behavior, not by chance or randomness; when running Assert.AreEqual, Pex detected a branch on the string equality that guarded the assertion failure. Pex then computed the input parameters to 'take' the other branch... and fail the assertion.

[TestMethod(), ...]
public void ChunkStringInt32_70312_151917_0_01()
{
    this.Chunk(((string)(null)), -1);
}
        
[TestMethod(), ...]
[PexUnexpectedException(typeof(AssertFailedException))]
public void ChunkStringInt32_70312_151917_0_02()
{
   string s0 = "";
   this.Chunk(((string)(s0)), -1);
}

Both tests get added automatically in the project, although it does not show up in the screencast.

A naive implementation of the chunker is written that would potentially fix the issue found.

public class Chunker {
    string value;
    int length, index;
    public Chunker(string value, int length) 
    {
        this.value = value;
        this.length = length;
    }
    internal string Next() 
    {
        string chunk = this.value.Substring(this.index, this.length);
        this.index += this.length;
        return chunk;
    }
}

Pex is run again. Pex finds the null reference issue because value is not validated and the ArgumentOutOfRangeException because index increases without bounds. More failures could have been found but Pex was configured to stop after 2 failures. In these particular cases where the input to a method breaks it's contract (triggers argument validation), Pex uses a precise data-flow analysis to deduce how and where an argument validation (i.e. pre-condition) should be added. In the screencast, although the error occurs in Next, the public constructor is the location where the argument should have been validated.

public Chunker(string value, int length) 
{
    // [Pex] begin preconditions
    if (value == null)
        throw new ArgumentNullException("value");
    if (length < 0 | value.Length < length)
        throw new ArgumentException("length < 0 | value.Length < length");
    // [Pex] end preconditions
    this.value = value;
    this.length = length;
}

Pex is run again and now reports the argument validation exceptions as failure. This occurs because Pex does not have any idea on how the user wants to triage the exceptions (expected or not?). The user can use a set of custom attributes to do this. In the screencast, the PexAllowedException attribute is used to state that

Pex is run again and silently emits tests with the ExpectedException attribute for the argument validation cases. This iteration continus a couple more times...

if (length <= 0 | value.Length > length)
    throw new ArgumentOutOfRangeException();

string chunk;
if (this.index > this.value.Length)
    chunk = null;
else
    chunk = this.value.Substring(this.index, this.length);

string chunk;
if (this.index > this.value.Length)
    chunk = null;
else if (this.index + this.length > this.value.Length)
    chunk = this.value.Substring(this.index);
else
    chunk = this.value.Substring(this.index, this.length);