Integrating a set of contract checking tools into Visual Studio
Integrating a set of contract checking tools into Visual Studio
复制标题
将一组合同检查工具集成到 Visual Studio 中
DOI：
10.1109/topi.2012.6229809
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
F. Logozzo
中科院分区：
文献类型：
--
作者：
M. Fähndrich;Mike Barnett;Daan Leijen;F. Logozzo
将工具和扩展集成到现有语言，编译器，辩论者和IDE中可能是困难，工作密集的，并且通常会导致一次性集成。在本文中，我们报告了我们建立和集成了设置为现有编程环境的CodeCecntract工具的经验。 CodeContract工具启用1）合同的作者（前提条件，后情况和对象不变性），2）仪器合同检查到代码中，3）静态检查合同的代码，4）可视化合同和结果。我们确定了集成的三个特征，使我们能够重复使用现有的编译器和IDE，将工具的覆盖范围增加到多种语言和目标平台，并在三个连续的C＃和Visual Studio上维护工具，并以很少的努力。这些原则是1）使用源嵌入新语言功能，2）使用目标分析和重写，以及3）使用通用插件将工具与IDE隔离。
Integrating tools and extensions into existing languages, compilers, debuggers, and IDEs can be difficult, work-intensive, 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), 2) 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.