How to instruct Pex to exploit class invariants specified with Code Contracts in generating objects?

Question

The PUT pattern doc (http://research.microsoft.com/en-us/projects/pex/patterns.pdf) states:

"As a side effect of defining a class invariant with the ContractInvariantMethod
attribute, Pex will configure instances of this class by directly setting the (private)
fields, and making sure that the invariant holds."

But when I do so, Pex doesn't seem to generate objects by setting the private fields. Do I need to do anything else specific?

Thanks!

Tao

Answer 1

The document also says: "The Code Contracts rewriter will insert calls to designated class invariant methods automatically at the end of all public methods when runtime checking of contracts is enabled."

Okay, we clearly have to clarify this portion of document. What is meant, and what you have to do, is the following:
 

Besides having a valid invariant method, annotated with [ContractInvariantMethod], and containing calls to Contract.Invariant(bool), you need to check “Perform Runtime Contract Checking” in the “Code Contracts” pane in the Project Properties.

---

---

Nikolai Tillmann - Tell us how you use Pex