你能详细说明AssumeInvariant实际上做了什么吗？ [英] Can you elaborate what AssumeInvariant actually does ?

问题描述

您好，我已阅读有关新的用户文档  AssumeInvariant。但是文档有点受限，我对它的作用感到有些困惑。据我所知，不变量我们声明布尔条件。但是在文档AssumeInvariant中，这需要一个T
作为对象参数。你能否进一步详细说明这个功能（希望有一个更好的例子）？

解决方案

据我了解，AssumeInvariant只是告诉静态分析器假设所有不变量在这一点上是正确的。

以下是文档的说法：

http://research.microsoft.com/en-us/projects/ contract / userdoc.pdf

静态检查器识别一个新的合同助手AssumeInvariant，它允许你在任意点假设一个对象的
不变量在你的程序中。对于某些静态检查器来说，这是一种解决办法。
限制。参见2.13节。

2.13中有一个代码示例。

Hello, I read the user documentation about new  AssumeInvariant. But the doc is somewhat limited and I am a bit puzzled about what it does. As far as I know as invariants we declare boolean conditions. But this in the doc AssumeInvariant takes a T as an object parameter. Can you please elaborate this functionality further (hopefully with a better example) ?

解决方案

As I understood it, AssumeInvariant simply tells the static anlyser to assume all invariants are true at that point.

Here's what the docs say:

http://research.microsoft.com/en-us/projects/contracts/userdoc.pdf

 The static checker recognizes a new contract helper AssumeInvariant that allows you to assume the
invariant of an object at arbitrary points in your program. It is a work-around for some static checker
limitations. See Section 2.13.

There's a code example in 2.13.

这篇关于你能详细说明AssumeInvariant实际上做了什么吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！