确保和循环的问题 [英] Problem with ensures and loop

问题描述

你好

 

在这个简单的代码中

private static void Test(string s, ref int pos)
{
  Contract.Requires(s != null);
  Contract.Requires(pos >= 0);
  Contract.Requires(pos < s.Length);
  Contract.Ensures(pos >= Contract.OldValue(pos));

  while (pos < s.Length)
  {
    pos++;
  }
}

推荐答案

我不知道为什么代码后置条件无法在给出的代码中证明，但是如果对代码进行以下修改，静态检查器似乎能够证明后置条件：

I don't know why the code postcondition can't be proven in the code given but the static checker seems to be able to prove the postcondition if you make the following modification to the code:

    private static void Test(string s, ref int pos)
    {
      Contract.Requires(s != null);
      Contract.Requires(pos >= 0);
      Contract.Requires(pos < s.Length);
      Contract.Ensures(pos >= Contract.OldValue(pos));

      int tmp = 0;
      while (pos < s.Length)
      {
        tmp++;
      }

      pos += tmp;
    }

这篇关于确保和循环的问题的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！