Static Verification for Code Contracts

Static Verification for Code Contracts
复制标题

代码合约的静态验证

DOI:
--
复制
发表时间:
2010
期刊:
Sensors Applications Symposium
影响因子:
--
通讯作者:
M. Fähndrich
M. Fähndrich
中科院分区:
--
文献类型:
--
作者:
M. Fähndrich

文献摘要

被引文献

相似文献

Microsoft Research 的 Code Contracts 项目 [3] 使 .NET 平台上的程序员能够使用现有语言(例如 C# 和 VisualBasic)编写规范。为了利用这些规范,我们提供了用于文档生成、运行时合约检查和静态合约验证的工具。 本次演讲详细介绍了静态契约检查器的总体方法,并研究了我们在何处以及如何权衡稳健性,以获得适用于成熟的面向对象中间语言(例如 .NET 通用中间语言)的实用工具。
The Code Contracts project [3] at Microsoft Research enables programmers on the .NET platform to author specifications in existing languages such as C# and VisualBasic. To take advantage of these specifications, we provide tools for documentation generation, runtime contract checking, and static contract verification. This talk details the overall approach of the static contract checker and examines where and how we trade-off soundness in order to obtain a practical tool that works on a full-fledged object-oriented intermediate language such as the .NET Common Intermediate Language.