可能的错误？ [英] Possible bug?

问题描述

我已经使用静态检查程序隔离了以下问题。在下面的示例中，验证结果不会引发错误确保错误。我使用代码约定属性窗格中的默认选项，我的代码合同版本是1.5.60502.11。

I have isolated the following problem with the static checker. In the example below the result of the verification is not raising a false ensure error. I am using the default options in the Code Contracts property pane and my Code Contracts version is 1.5.60502.11.

	class Program
	{
		public int size;

		static void Main(string[] args)
		{
			var program = new Program();
			program.Test();
		}

		public void Test()
		{
			Contract.Requires(size > 0);
			Contract.Ensures(size > 0);

			size = size - 1;
		}
	}

您有什么想法吗？

谢谢！

推荐答案

您是否使用"推断要求"运行它？ on？

Are you running it with the "Infer requires" on?

这就是发生的事情。

静态检查器会推断无法证明确保。它还将意识到你需要前提条件大小> 1，否则程序肯定是错误的（这是必要的前提条件）。

The static checker will infer that the ensures cannot be proven. It will also realize that you need the precondition size > 1, otherwise the program will be definitely wrong (it's a necessary precondition).

使用"推断要求"打开，静态检查器会将前提条件传播给调用者，然后发出警告。

With the "infer requires" switch on, the static checker will propagate the precondition to the callers, and at that point emit the warning.

所以，如果仔细查看"输出"窗口，你会发现

So, if you look carefully in the Output window, you will find a

"需要未经证实（this.size -1）> 0"

"requires unproven (this.size -1) > 0"

对应于Main中的program.Test（）。

corresponding to program.Test() in Main.

你不会在曲线中得到它，因为VS只会显示一个警告

You will not get it in the squiggles, as VS will show only one warning

ciao

f

这篇关于可能的错误？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！