Ever wanted to host a constraint solver in your web page? It is now possible to host the http://rise4fun.com web site in an iframe (without the chrome). It just looks like this:

<iframe allowtransparency="true" frameborder="0" style="width:600px;height:800px" src=”http://rise4fun.com/z3?frame=1&menu=0”></iframe>

You can learn more about this feature at our documentation page.

http://rise4fun.com/ is a web front end to a number of tools produced by the RiSE group. It also exposesREST services that allow you to play with the tools from your favorite environment.

Rendering DOT graphs to SVG

DOT is a popular language to describe graphs. It can be rendered into SVG using the MSAGL tool on http://rise4fun.com . To do so, you simply need to do a POST query to http://rise4fun.com/services.svc/ask/agl where the dot code is passed in the request body. rise4fun returns SVG markup that can be viewed in browsers that support it.

Wondering what graph SVG look like? Check out http://rise4fun.com/agl/cilreader to see this beautiful graph. Make sure to zoom out as the graph is rather laaaaaarge.

Cheers, Peli

We have just published a new game where you have to figure out the secret regular expression. Try it out, you might be surprised what you will find there.

http://www.rise4fun.com/Rex

Nikolai Tillmann announced it on our page, he just finished integrating Rex in to Pex….

Picture-in-Picture is a very cool feature of Camtasia that allows to embed a movie stream into a screencast. It makes the screencast more lively while keeping a perfect quality of the computer screen. You've seen this kind of screencast all over the place on Channel9. Unfortunately, this feature was limited for screen recording and whiteboard session would never look that good since we had to zoom in and out to capture… not anymore.

We invested in an eBeam device that can capture the pen strokes on any whiteboard and display them on the computer. Using this device, we can do Picture-in-Picture for Whiteboard recordings! Using that device, we use the following setup: a camera on a tripod to record the person on the whiteboard, the eBeam capture software running and Camtasia recording the computer screen. The first result of this experiment is the first episode of a new show, The Verification Corner, where Rustan Leino explains Loop Invariants. The other benefit of recording the whiteboard is that you get a hard copy out it. If you go to the Channel9 page, you’ll see that you can also download a .pdf or .pptx of all the whiteboard that Rustan wrote during the session… Go check it out and tell us what you think…

We just made a quick release to fix another installer issue related to missing packages. Along the way, we’ve added an Exploration Tree View and Partial Stubs support.

Exploration Tree View

The exploration tree view displays the list of explorations to be executed, running and finished. It serves as a progress indicator but also as a smooth result explorer. When browsing through the tree, Pex will synchronize the exploration result view and the tree view.

The tree view populates each namespace with the fixture types and exploration methods, and provide a visual feedback on the progress of Pex.

When you browse through the exploration and generated test nodes, Pex automatically synchronizes the exploration result display. This makes it really easy to start from an high-level view of the failures and drill into a particular generated test, with stack trace and parameter table.

Partial Stubs

Stubs lets you call the base class implementation of methods as a fallback behavior. This functionality is commonly referred as Partial Mocks or Partial Stubs and is useful to test abstract classes in isolation. Stubs inheriting from classes have a “CallBase” property that can turn this mode on and off.

Let see this with the RhinoMocks example on partial mocks. Given an abstract ProcessorBase class,

we write a test for the Inc method. To do so, we provide a stub implementation of Add that simply increment a counter.

Miscellaneous

• PexAssume/PexAssert.EnumIsDefine checks that a particular value is defined in an enum.
• Missing OpenMP files in the installer break Pex.

Poll: should we skip 0.13 and go straight for 0.14? :)

For the last couple of weeks, I given on helping hand to Herman Venter to set up the open-source-MS-PL-super-cool-Common Compiler Infrastructure (CCI) project.

You’ve may have heard and probably used different incarnations of the CCI in the past: the FxCop introspection engine, ILMerge, Spec# or Code Contracts use CCI in same ways. CCI is a set of tools and components that are useful to build compilers: readers and writers for MSIL and symbol files, and more. With CCI, you can now easily write your own crazy aspect oriented programming framework, inspect assemblies without reflection etc…  Just sync the sources, build it, tweak it, etc… It’s all there on codeplex at http://ccimetadata.codeplex.com.

Download the new version!

Today we’ve released a new release of Pex on DevLabs and on our academic downloads. This highlights of this release are: NUnit, MbUnit and xUnit.net support out of the box, writing parameterized unit tests in VisualBasic.NET and F#, better Code Contracts support. As always, if we encourage you to send us feedback, bugs, stories on our forums at http://social.msdn.microsoft.com/Forums/en-US/pex/threads/ .

NUnit, MbUnit and xUnit.net supported out of the box

Pex now supports MSTest, NUnit, MbUnit and xUnit.net out of the box. Pex will automatically detect which framework you are using by inspecting the assembly reference list, and automatically save the generated tests decorated with the correct attributes for that framework.

The default test framework can also be specified through the global options (Tools –> Options –> Pex –> enter the test framework name in TestFramework).

Writing Parameterized Unit Tests in VisualBasic.NET

While the Pex white box analysis engine works at the MSIL level, Pex only emits C# code for now. In previous releases, this limitation made it impossible to use Pex parameterized unit tests from non-C# code. In this release, we have worked around this problem by automatically saving the generated tests in a ‘satellite’ C# project.

Let’s see this with an example. The screenshot below shows a single VisualBasic.NET test project with a Pex parameterized unit test:

We can right-click in the HelloTest.Hello method and select “Run Pex Explorations”:

At this point, Pex will start exploring the test in the background as usual. This is where the new support comes in: When a generated test comes back to Visual Studio, Pex will save it in a separate C# project automatically (after asking you where to drop the new project):

The generated tests are now ready to be run just as any other unit tests!

Writing Parameterized Unit Tests from F#

Similarly to VisualBasic.NET, we’ve made improvements in our infrastructure to enable writing parameterized unit tests in F#. Let’s see this with a familiar example. We have a single F# library that has xUnit.net unit tests and reference Microsoft.Pex.Framework (project Library2 below). In that project, we add a parameterized unit test (hello_test):

We can right-click on the test method name and Pex will start the exploration of that test in the background. Because of the limitations of the F# project system, you absolutely need to right-click on the method name in F# if you want contextual test selection to work. Because the project is already referencing xunit.dll, Pex will also automatically detect that you are using xUnit.net and use that framework. When the first test case comes back to VisualStudio, Pex saves it in a separate C# project:

The tests are saved in the generated test project and ready to be run by your favorite test runner!

PexObserve: Observing values, Asserting values

We’ve completely re-factored the way values can be logged on the table or saved as assertions in the generated tests. The following example shows various ways to log and assert values:

In the Observe method, we use the return value and out parameter output to automatically log and assert those values. Additionally, we add “view input” on the fly to the parameter table through the ValueForViewing method, and we add “check input” to be asserted through the ValueAtEndOfTest method. After running Pex, we get the following results:

As expected, input, ‘view input’, output and result show up in the parameter table.

In the generated test, we see assertions for the return value, out parameters and other values passed through the ValueAtEndOfTest method.

Code Contracts : Reproducible generated tests

When Pex generates a unit test that relied on a runtime contract, Pex also adds a check to the unit test which validates that the contracts have been injected into the code by the contracts rewriter. If the code is not rewritten when re-executing the unit test, it is marked as inconclusive. You will appreciate this behavior when you run your unit tests both in Release and in Debug builds, which usually differ in how contracts get injected.

Code Contracts:  Automatic filtering of the contract violations

When Pex generates a test that violates a Code Contract pre-condition (i.e. Contract.Requires), there are basically two scenarios: the precondition was on top of the stack and should be considered as an expected exception; or it is a nested exception and should be considered as a bug. Pex provides a default exception filtering that implements this behavior.

Stubs: simplified syntax

We’ve considerably simplified the syntax of stubs by removing the ‘this’ parameter from the stub delegate definition. Let’s illustrate this with a test that stubs the ‘ReadAllText’ method of a fictitious ‘IFileSystem’ interface. 

Stubs: generic methods

The Stubs framework now supports stubbing generic methods by providing particular instantiations of that method. In the following example, the generic Bar<T> method is stubbed for the particular Bar<int> instantiation:

Stubs and Pex: Pex will choose the stubs behavior by default

We provide a new custom attribute, PexChooseAsStubFallbackBehaviorAttribute, that hooks Pex choices to the Stub fallback behavior. To illustrate what this means, let’s modify slightly the example above by removing the stub of ReadAllText:

If this test was to be run without the PexChooseAsStubFallbackBehavior attribute, it would throw a StubNotImplementedException. However, with the PexChooseAsStubFallbackBehavior attribute, the fallback behavior calls into PexChoose to ask Pex for a new string. In this example in particular, on each call to ReadAllText, Pex will generate a new string for the result. You can see this string as a new parameter to the parameterized unit test. Therefore, when we run this test under Pex, we see different behavior happening, including the “hello world” file:

Note that all the necessary attributes are added at the assembly level by the Pex Wizard.

Miscellanous bug fixes and improvements

• [fixed] Dialogs do not render correctly under high DPI
• When a generic parameterized unit tests does not have any generic argument instantiations, Pex makes a guess for you.
• When a test parameter is an interface or an abstract class, Pex now searches the known assemblies for implementations and concrete classes. In particular, that means that Pex will often automatically use the automatically generated Stubs implementations for interfaces or abstract classes.
• Static parameterized unit tests are supported (if static tests are supported by your test framework)
• Better solving of decimal and floating point constraints. We will report on the details later.

Breaking Changes

• The PexFactoryClassAttribute is no longer needed and has been removed. Now, Pex will pick up object factory methods marked with the PexFactoryMethodAttribute from any static class in the test project containing the parameterized unit tests. If the generated tests are stored in a separate project, that project is not searched.
• The PexStore API has been renamed to PexObserve.
• Pex is compatible with Code Contracts versions strictly newer than v1.1.20309.13. Unfortunately, v1.1.20309.13 is the currently available version of Code Contracts. The Code Contracts team is planning on a release soon.

Happy Pexing!

A while ago at PDC, a couple of my colleagues presented CHESS but unfortunately weren’t ready to release it. Well, you don’t have to wait anymore: CHESS is now available for download at DevLabs for Visual Studio 2008 Team Dev or Team Test. CHESS comes under the same pre-release license as Pex or under an academic license.

CHESS = Unit Testing of Concurrent Programs

CHESS is a tool that finds and reproduces “Heisenbugs” in concurrent programs (both Win32 and .NET)… You know those kind of bugs that do not reproduce under the debugger or only in production environment, the kind of bugs where you scratch your head for days in front of a process dump before giving up.

I also recently recorded a great ‘getting started’ CHESS tutorial for CHESS in Visual Studio Unit Test: you can take a unit test*** and turn it into a CHESS test by adding the [HostType(“Chess”)] attribute!

*** That unit test should involve threads, otherwise CHESS will have not effect.

CHESS and Pex

In order to control the scheduling of .NET programs, CHESS instruments the threading APIs using ExtendedReflection, the code instrumentation framework that was built for Pex. In the future, we would also like to combine both approach to explore data inputs and thread schedules together.

Well enough said… go and try it out!