标签：c code-contracts design-by-contract spec

我想在C#中实现DBC.我面对的是Spec#和Code Contract.
Spec#和Code Contract有什么区别？

解决方法:

这是从Code Contracts FAQs at Microsoft Research：

Do Code Contracts have anything to do with Spec#?

Code Contracts is a spin-off from the Spec# project. Spec#’s research focus is to
understand the meaning of object invariants in the presence of
inheritance, call backs, aliasing and multi-threading. Spec# is a
superset of C# v2.0 and uses a source level rewriter to weave the
contracts into the code. It uses verification condition generation and
a theorem prover for the static verification of Spec# code. But
dealing soundly with all the complex issues around maintaining object
invariants has a price: verification becomes non-trivial. That’s why
Spec# also needs an ownership discipline to know which objects may
alias or cannot alias each other.

Code Contracts is the result of learning from Spec# what works and
what doesn’t. Unlike Spec#, Code Contracts are language agnostic, and
thus work across all .NET languages, from VB to C# to F#. The rewriter
works on MSIL and thus had no dependency on particular compilers. Its
static analysis engine uses abstract interpretation, which is much
faster and more predictable than verification; furthermore abstract
interpretation infers loop invariants and method contracts, which
helps in adoption and ease of use of Code Contracts.

因此,代码合约似乎将成为未来更“支持”的工具.

标签：c,code-contracts,design-by-contract,spec
来源： https://codeday.me/bug/20190624/1276901.html

本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享；
2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关；
3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关；
4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除；
5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。