New Release of Pex and Code Contracts

Microsoft Research has released new versions of Pex and Code Contracts. You are required to go to DevLabs to download the commercial evaluation of Pex and Code Contracts. You can retrieve the academic version of Pex and Code Contracts from Microsoft Research.

Pex

Pex v0.21.50115.2 has a few bug fixes in it, but there is a major change to the Stubs framework. It has been renamed to Moles framework. ‘Stubs’ is now named ‘Moles’ and ‘Beaver’ is now named ‘Behaved’. Due to this change, any existing .stubx files will no longer work. Here are the steps to migrate from the previous version of Pex (from the release notes):

change the project reference from Microsoft.Stubs.Framework.dll to Microsoft.Moles.Framework.dll

rename all .stubx files to .moles, and

• rename the top <Stubs xml element to <Moles.
• Change the XSD namespace to http://schemas.microsoft.com/moles/2010/
• Right click on the .moles file in the Solution Explorer and change the Custom Tool Name to ‘MolesGenerator’.
• Delete all the nested files under the .moles files

Remove references to any compiled .Stubs.dll files in your project

In general, remove all .Stubs.dll, .Stubs.xml files from your projects.

Rename .Stubs namespace suffixes to .Moles.

replace all [HostType(“Pex”)] attribute with [HostType(“Moles”)]

in PexAssemblyInfo.cs,

• rename using Microsoft.Pex.Framework.Stubs to Microsoft.Pex.Framework.Moles
• rename [assembly: PexChooseAsStubFallbackBehavior] to [assembly: PexChooseAsBehavedCurrentBehavior]
• rename [assembly: PexChooseAsStubFallbackBehavior] to [assembly: PexChooseAsMoleCurrentBehavior]

In general, the ‘Fallback’ prefix has been dropped in the following methods:

• rename FallbackAsNotImplemented() to BehaveAsNotImplemented()
• rename class MoleFallbackBehavior to MoleBehaviors
• rename class StubFallbackBehavior to BehavedBehavors

Code Contracts

Code Contracts 1.2.30118.5 is a quick bug fix to address issues with last week’s release. I’m kind of curious about this one fix: “Auto-properties containing && ||, or ? should now be handled properly.” How does an auto-property get one of those symbols… obfuscation?

Last week’s released dropped support for Silverlight 2 and adds it for Silverlight 4. A new set of reference assemblies have been added to allow contracts on newer APIs. The issues with referencing v3.5 assemblies with contracts from v4 projects are now corrected.

An interesting development is the ability to use auto properties with contracts. Using invariants, which now must be private, on an automatic property are assigned to pre and post conditions of the compiler generated getter and setter methods (which was the reason for the quick bug fix).