Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Integrating a Set of Contract Checking Tools into Visual Studio

Manuel Fahndrich, Michael Barnett, Daan Leijen, and Francesco Logozzo


Integrating tools and extensions into existing languages,

compilers, debuggers, and IDEs can be difficult, workintensive,

and often results in a one-off integration. In this

paper, we report on our experience of building and integrating

the CodeContract tool set into an existing programming

environment. The CodeContract tools enable 1) authoring of

contracts (preconditions, postconditions, and object invariants),

  1. Instrumenting contract checks into code, 3) statically checking

code against contracts, and 4) visualizing contracts and

results. We identify three characteristics of our integration that

allowed us to reuse existing compilers and IDEs, increase the

reach of our tools to multiple languages and target platforms,

and maintain the tools over three consecutive versions of C#

and Visual Studio with little effort. These principles are 1)

use source embedding for new language features, 2) use target

analysis and rewriting, and 3) use generic plug-ins to isolate

tools from the IDE.


Publication typeInproceedings
Published inProceedings of the 2012 Second International Workshop on Developing Tools as Plug-ins (TOPI 2012)
> Publications > Integrating a Set of Contract Checking Tools into Visual Studio