确保rot13（rot13（输入））==输入 [英] Ensuring rot13(rot13(input)) == input

问题描述

嘿，

我一直在玩各种模型检查器，主要是相对"玩具"。程序（比如这个！），并且在我看来有点令人惊讶。

I've been playing around a little with various model checkers, mostly with relatively "toy" programs (such as this!), and have hit what seems to me to be a bit surprising.

给出以下内容：

using System.Diagnostics.Contracts;

namespace ROT13LIB
{
    public class ROT13
    {
        [Pure]
        static public char rot13(char i)
        {
            Contract.Ensures(i.Equals(rot13(Contract.Result<char>())));

            char offset;
            if ('a' <= i && i <= 'z')
                offset = 'a';
            else if ('A' <= i && i <= 'Z')
                offset = 'A';
            else
                return i;

            if (i - offset < 13)
                return (char)(i + 13);
            else
                return (char)(i - 13);
        }
    }
}

我最终得到：

CodeContracts: ROT13LIB: Validated: 40.0 %
CodeContracts: ROT13LIB: Checked 5 assertions: 2 correct 3 unknown
CodeContracts: ROT13LIB: Contract density: 0.40
CodeContracts: ROT13LIB: Total methods analyzed 3
CodeContracts: ROT13LIB: Methods with 0 warnings 2
CodeContracts: ROT13LIB: Total time 7.081sec. 2360ms/method
CodeContracts: ROT13LIB: Retained 0 preconditions after filtering
CodeContracts: ROT13LIB: Inferred 0 object invariants
CodeContracts: ROT13LIB: Retained 0 object invariants after filtering
CodeContracts: ROT13LIB: Discovered 2 postconditions to suggest
CodeContracts: ROT13LIB: Retained 2 postconditions after filtering
CodeContracts: ROT13LIB: Detected 0 code fixes
CodeContracts: ROT13LIB: Proof obligations with a code fix: 0
c:\users\gsnedders\documents\visual studio 2010\Projects\ROT13\ROT13LIB\ROT13.cs(21,17): error : CodeContracts: ensures unproven: i.Equals(rot13(Contract.Result<char>()))
c:\users\gsnedders\documents\visual studio 2010\Projects\ROT13\ROT13LIB\ROT13.cs(10,13): error :   + location related to previous warning
c:\users\gsnedders\documents\visual studio 2010\Projects\ROT13\ROT13LIB\ROT13.cs(23,17): error : CodeContracts: ensures unproven: i.Equals(rot13(Contract.Result<char>()))
c:\users\gsnedders\documents\visual studio 2010\Projects\ROT13\ROT13LIB\ROT13.cs(10,13): error :   + location related to previous warning
c:\users\gsnedders\documents\visual studio 2010\Projects\ROT13\ROT13LIB\ROT13.cs(18,17): error : CodeContracts: ensures unproven: i.Equals(rot13(Contract.Result<char>()))
c:\users\gsnedders\documents\visual studio 2010\Projects\ROT13\ROT13LIB\ROT13.cs(10,13): error :   + location related to previous warning
C:\Users\gsnedders\Desktop\ROT13LIB.dll(1,1): message : CodeContracts: Checked 5 assertions: 2 correct 3 unknown
CodeContracts: ROT13LIB: 
CodeContracts: ROT13LIB: Background contract analysis done.

所有这些不同的"确保未经证实"行是返回语句的行。

All these various "ensures unproven" lines are those of the return statements.

有没有人有任何建议如何确保rot13（rot13（i））== i断言？ （另外，在一旁，后置条件"建议"建议在哪里？我无法在任何地方找到它们？）

Does anyone have any suggestion how to ensure the rot13(rot13(i)) == i assertion? (Also, on an aside, where are the postconditions "to suggest" suggested? I can't find them anywhere?)

推荐答案

你无法通过假设/保证方法证明上述后置条件，这是静态检查器使用的方法。

Hi, there is no way you can prove the postcondition above by only using an assume/guarantee approach, which is the one used by the static checker.

要证明后置条件，你需要在后置条件下内联rot13的主体，这是模型检查器可能做的。这种方法的问题是爆炸（空间和时间）导致（通常）模型检查器超时。

To prove the postcondition, you need to inline the body of rot13 in the postcondition, which is what model checker may do. The problem with such an approach is the blow up (in space and time) which causes (in general) model checkers to timeout.

如果你想证明这个属性，可以通过简单地插入代码来实现，如下所示。

If you want to prove the property, you can do it by simply inlining the code, as below.

      static public char rot13Ex(char i)
      {
        //Contract.Ensures(i == rot13Ex(rot13Ex(Contract.Result<char>())));

        char i0 = i;
        char offset, result;

        // rot13(i)
        if ('a' <= i && i <= 'z')
          offset = 'a';
        else if ('A' <= i && i <= 'Z')
          offset = 'A';
        else
        {
          result = i;
          goto next;
        //  return i;
        }

        if (i - offset < 13)
        {
          result =  (char)(i + 13);
          goto next;
        }
        else
        {
          result = (char)(i - 13);
          goto next;
        }

      next:
        // rot13(rot13)
        i = result;
        if ('a' <= i && i <= 'z')
          offset = 'a';
        else if ('A' <= i && i <= 'Z')
          offset = 'A';
        else
        {
          result = i;
          goto check;
        }
        if (i - offset < 13)
        {
          result = (char)(i + 13);
          goto check;
        }
        else
        {
          result =  (char)(i - 13);
          goto check;
        }
      check:
        Contract.Assert(i0 == result);
        ;

        return result;
      }

 

 

这篇关于确保rot13（rot13（输入））==输入的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！