Pex 提出了一个解决 Moles 错误的解决方案

Question

我尝试使用 Pex 探索以下方法：

public float MultiplyFloat(float a, float j)
{
    if (a * a == 2)
    {
    if (j == 123)
    {
        a = 2;
    }
    }
    else
    a = 3;

    return 3;
}

我知道 Z3 是一个线性算术求解器，不支持浮点，但 Visual Studio 2010 插件中的 Pex 向导建议我使用“Moles Type”，我使用此建议并创建 Pex 向导：

1) Microsoft.Pex.Framework.moles 文件

<Moles xmlns="http://schemas.microsoft.com/moles/2010/">
  <Assembly Name="Microsoft.Pex.Framework" />
</Moles>

2) 准备好的类：__TestabilityHelperPreparation

using System;
using Microsoft.Pex.Framework;
using Microsoft.Pex.Engine.Symbols.Moles;
using Microsoft.Pex.Engine.Symbols;

namespace Microsoft.Pex.Engine.Symbols.Preparations
{
    /// <summary>Contains a method to prepare the type __TestabilityHelper</summary>
    public static partial class __TestabilityHelperPreparation
    {
        /// <summary>Prepares the environment (and the moles) before executing any method of the prepared type __TestabilityHelper</summary>
        [PexPreparationMethod(typeof(__TestabilityHelper))]
        public static void Prepare()
        {
            M__TestabilityHelper.BehaveAsCurrent();
            // TODO: use Moles to replace API that call into the environment
        }
    }
}

但编译时出现以下错误：

C:\Program Files (x86)\Microsoft\Contracts\MsBuild\v4.0\Microsoft.CodeContracts.targets(274,5): error MSB3073: uscita dal comando ""C:\Program Files (x86)\Microsoft SDKs\Windows\v8.0A\Bin\sn.exe" /R "o\Microsoft.Pex.Framework.Moles.dll" "m.g.snk"" con codice 9009. [D:\BenchMarkTesterToolLib.Tests02\obj\Debug\Moles\mpf\m.g.csproj]

Moles compilation FAILED - 58,028916314783s

C:\Program Files\Microsoft Moles\bin\Microsoft.Moles.targets(79,5): error MSB3073: uscita dal comando ""C:\Program Files\Microsoft Moles\bin\moles.exe" @D:\BenchMarkTesterToolLib.Tests02\obj\Debug\Moles\moles.args" con codice -1002.

那么，我是一个错误还是 Pex 向我建议了一个错误的解决方案？

谢谢。

Answer 1

问题实际上出在代码合同上，它运行了错误的sn 版本。这已在最新版本的代码合同中得到修复。因此，请尝试更新代码合同并重试。