يجب أن يكون عقود التعليمات البرمجية المدقق الثابت قادرا على التحقق من الحدود الحسابية؟

Question

(أيضا نشر على منتدى MSDN - لكن هذا لا يحصل على الكثير من حركة المرور، بقدر ما أستطيع أن أرى.)

لقد كنت أحاول تقديم مثال على Assert و Assume. وبعد إليك الرمز الذي حصلت عليه:

public static int RollDice(Random rng)
{
    Contract.Ensures(Contract.Result<int>() >= 2 &&
                     Contract.Result<int>() <= 12);

    if (rng == null)
    {
        rng = new Random();
    }
    Contract.Assert(rng != null);

    int firstRoll = rng.Next(1, 7);
    Contract.Assume(firstRoll >= 1 && firstRoll <= 6);

    int secondRoll = rng.Next(1, 7);
    Contract.Assume(secondRoll >= 1 && secondRoll <= 6);

    return firstRoll + secondRoll;
}

(العمل حول القدرة على المرور في مرجع فارغ بدلا من القائمة Random المرجع التربوي البحري، بالطبع.)

كنت آمل أن يكون المدقق يعرف ذلك firstRoll و secondRoll كانت كل في النطاق [1, 6], ، سيكون قادرا على العمل أن المبلغ كان في النطاق [2, 12].

هل هذا أمل غير معقول؟ أدرك أنه عمل صعب، والعمل بالضبط ما قد يحدث ... لكنني كنت آمل أن يكون المدقق ذكيا بما فيه الكفاية :)

إذا لم يكن هذا غير مدعوم الآن، فهل أي شخص هنا يعرف ما إذا كان من المحتمل أن يتم دعمه في مستقبل ISH القريب؟

تحرير: لقد وجدت الآن أن هناك خيارات معقدة للغاية للحساب في المدقق الاستقرائي. باستخدام مربع النص "المتقدمة" يمكنني تجربته من Visual Studio، ولكن لا يوجد تفسير مناسب لما يفعلونه، بقدر ما أستطيع أن أقول.

Answer 1

لقد حصلت على إجابة على منتدى MSDN. اتضح أنني كنت تقريبا هناك. أساسا يعمل المدقق الثابت بشكل أفضل إذا قمت بتقسيم العقود "وإد". لذلك، إذا قمنا بتغيير التعليمات البرمجية إلى هذا:

public static int RollDice(Random rng)
{
    Contract.Ensures(Contract.Result<int>() >= 2);
    Contract.Ensures(Contract.Result<int>() <= 12);

    if (rng == null)
    {
        rng = new Random();
    }
    Contract.Assert(rng != null);

    int firstRoll = rng.Next(1, 7);
    Contract.Assume(firstRoll >= 1);
    Contract.Assume(firstRoll <= 6);
    int secondRoll = rng.Next(1, 7);
    Contract.Assume(secondRoll >= 1);
    Contract.Assume(secondRoll <= 6);

    return firstRoll + secondRoll;
}

التي تعمل دون أي مشاكل. وهذا يعني أيضا أن المثال أكثر فائدة، لأنها تسلط الضوء على النقطة التي يكون المدقق هل العمل بشكل أفضل مع الانفصال عن العقود.

Answer 2

لا أعرف عن أداة مدقق مدقق MS، ولكن تحليل النطاق هو تقنية تحليل ثابت قياسي؛ يستخدم على نطاق واسع في أدوات التحليل الثابت التجارية للتحقق من أن التعبيرات الكارية قانونية.

لدى MS Research سجل حافل جيد في هذا النوع من التحليلات الثابتة، ولذا فإنني أتوقع أن أفعل تحليل هذا النطاق هو هدف مدقق العقود، حتى لو لم يتم التحقق حاليا.