1

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 Wizard を作成します。

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 は私に間違った解決策を提案していますか?

ありがとう。

4

1 に答える 1

1

問題は実際には Code Contracts にあり、間違ったバージョンの を実行していsnます。これは、Code Contracts の最新バージョンで修正されています。そのため、Code Contracts を更新して、もう一度やり直してください。

于 2012-11-06T11:33:39.697 に答える