Contract.Requires throwing pex errors [duplicate]

Question

Possible Duplicate:
How Do You Configure Pex to Respect Code Contracts?

Currently, when I run a pex exploration, the code contracts I created in my classes are being treated as errors in the pex exploration results. I thought when you ran pex exploration using code contracts the contract failures should be treated as expected behavior. Here is the code causing the exceptions.

Test Method:

[PexMethod]
public void TestEquality(Guid userId, string username, string password, string securityQuestion, string securityAnswer)
{
    UserSecurity user = UserTools.CreateUser(Guid.NewGuid(), username, password, securityQuestion, securityAnswer);

    bool passwordResult = UserTools.VerifyInput(password, user.Password, user.PasswordSalt);
    bool securityAnswerResult = UserTools.VerifyInput(securityAnswer, user.SecurityAnswer, user.SecurityAnswerSalt);

    Assert.IsTrue(passwordResult, "Password did not correctly re-hash");
    Assert.IsTrue(securityAnswerResult, "Security Answer did not correctly re-hash");
}

Failing method call:

public static UserSecurity CreateUser(Guid userId, string username, string password, string securityQuestion, string securityAnswer)
{
    Contract.Requires(userId != Guid.Empty);
    Contract.Requires(!string.IsNullOrWhiteSpace(username));
    Contract.Requires(!string.IsNullOrWhiteSpace(password));
    Contract.Requires(!string.IsNullOrWhiteSpace(securityQuestion));
    Contract.Requires(!string.IsNullOrWhiteSpace(securityAnswer));
    Contract.Ensures(Contract.Result<UserSecurity>() != null);

    byte[] passwordSalt;
    byte[] securityAnswerSalt;

    return new UserSecurity
               {
                   UserId = userId,
                   Username = username,
                   Password = SecurityUtilities.GenerateHash(password, out passwordSalt),
                   PasswordSalt = passwordSalt,
                   SecurityQuestion = securityQuestion,
                   SecurityAnswer = SecurityUtilities.GenerateHash(securityAnswer, out securityAnswerSalt),
                   SecurityAnswerSalt = securityAnswerSalt,
               };
}

--- Description

failing test: ContractException, Precondition failed: !string.IsNullOrWhiteSpace(username)

Guid s0
   = new Guid(default(int), (short)32, (short)32, default(byte), default(byte), 
              default(byte), default(byte), default(byte), 
              default(byte), default(byte), default(byte));
this.TestEquality(s0, (string)null, (string)null, (string)null, (string)null);


[TestMethod]
[PexGeneratedBy(typeof(HashTests))]
[PexRaisedContractException]
public void TestEqualityThrowsContractException173()
{
    Guid s0
       = new Guid(default(int), (short)32, (short)32, default(byte), default(byte), 
                  default(byte), default(byte), default(byte), 
                  default(byte), default(byte), default(byte));
    this.TestEquality(s0, (string)null, (string)null, (string)null, (string)null);
}

Sclerodermatous

Does the PEX team even monitor this forum? Or is there no more PEX team? – Sclerodermatous

I would not call this the "pex forum", even though someone from "them" might check here. Looks like this is the forum. – Bait

I don't think they respond there anymore. On the pex home page they make a note that the forums have been moved to stackoverflow. pex home page – Sclerodermatous

Ups, should have payed more attention. There is (of course) even a post in the old forum about that migration to SO. Sorry. – Bait

It's all good! I wasn't even able to find their old forum, so thanks for that. :) – Sclerodermatous

Answer 1

My understanding, from my limited experience with Pex, is that the Contract methods define the preconditions for reaching the method they are in. So, when you say

Contract.Requires(!string.IsNullOrWhiteSpace(username));

you are saying that there should be no way that statement can be reached with a null or whitespace username parameter. Pex is basically saying that you're wrong. This is one thing Pex is really good for. It means that you have the potential for a NullReferenceException or that you are not checking for an empty/whitespace username in some call to your CreateUser method. Your task, then, is to find where. You can either fix the problem by handling the null/whitespace username in the CreateUser method, then getting rid of the Contract.Requires for it, or by ensuring that all callers of CreateUser pass a non-null, non-empty username. The better choice depends on your situation, I think, but in nearly all cases, I would handle the null/whitespace username in the CreateUser method. That way, you can handle the error gracefully in one place in your code.

Of course, you really should see which caller can pass null or whitespace, since this could indicate a user input validation issue, among other potential problems.

Flirtatious

That is correct for Code contracts. However, when you utilize PEX to perform parameterized unit tests, it should be treating the code contracts as expected behavior. So even though the contract would throw an exception at runtime, pex treats this exception as expected. This use to be the case for pex unit tests. I think this may be a bug with the exploration results. – Sclerodermatous

@Joshua Dale See pages 10-11 of research.microsoft.com/en-us/projects/pex/pexandcontracts.pdf. What is your setting for "Perform Runtime Contract Checking"? – Flirtatious

Contracts are turned on for the target project (I also enabled it for the test project just to be sure). Also I am getting a ContractException currently so code contracts are enabled. – Sclerodermatous

I'd strongly advise against handling null/whitespace inside the CreateUser. The method cannot perform it's job without valid information and would need to throw an exception anyway - which is exactly the kind of situation ideal for defining pre-conditions in the first place. – Hyperdulia

@Morten Mertner I'm not sure what you are saying. Why wouldn't I place a precondition in that method? – Sclerodermatous

Answer 2

I find that if you use standard contract rewriter, untick assert on failure and let your code thron ArgumentNullException by using a typed Requires argument.

contract.Requires<ArgumentNullException>(i!=null);

when you do this the methods will throw argumentnullexceptions ... pex behaves perfectly well with them.

At compile time you still get contract checking and static checking as you would expect.

It does look like PexRaisedContractException isn't behaving with how you use it. I can't say i use that attribute though. I guess from your perspective my way is a work around ;)

EDIT: Pex should generate this test, but the test should throw the error and that should cause the test to pass. the fact this is not working suggests to me that the rewriter isn't working or that the exception being thrown is not the exception type that the attribute is looking for.

Danita

When using code contracts and pex, pex uses contract failures as expected exceptions and marks them green in the explorations. Your fix does work, but you gain no benefit in using pex and code contracts together. – Sclerodermatous

'You gain no benefit from using Pex and Contracts' that is rubbish. Using these 2 technologies in the way that i am doing has been the single largest advancement in my code quality ever for me. For someone who is unable to get it to work that is a fairly dogmatic statement. Even if you did mean additional benefit, i still disagree because contracts give me compile time checking and pex gives me a great tool for exploratory testing. I get bored of writing tests for nulls .... – Danita

I'm sorry. I didn't mean to downplay your fix, which works just fine. I was simply stating it isn't behaving like it use to. And getting supporthas been more problematic than it use to with the pex team. – Sclerodermatous

totally agreed about the support part ;) It took me awhile to convince people that pex wasn't dead ... but with the premium requirement on static checking on code contracts its no wonder this stuff is a hard sell. – Danita

Agreed. It is a great product that lacks transparency. I heard Moles is holding back pex updates. I can't remember where I heard that though. – Sclerodermatous