코드 계약 계약 정적 검사기가 산술 바운드를 확인할 수 있어야합니까?

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].

이것이 불합리한 희망입니까? 나는 그것이 까다로운 사업이라는 것을 알고 있습니다. 정확히 무슨 일이 일어날 지 정확히 해결합니다 ...하지만 체커가 충분히 똑똑하기를 바랐습니다 :)

이것이 지금 지원되지 않는다면, 여기에있는 사람이 가까운 미래에 지원 될 가능성이 있는지 아는 사람이 있습니까?

편집 : 이제 정적 체커에 산술에 대한 매우 복잡한 옵션이 있음을 발견했습니다. "고급"텍스트 상자를 사용하여 Visual Studio에서 시도해 볼 수 있지만, 내가 말할 수있는 한 그들이하는 일에 대한 괜찮은 설명은 없습니다.

Answer 1

MSDN 포럼에 대한 답변을 받았습니다. 내가 거의 거기에 있었다는 것이 밝혀졌습니다. 기본적으로 정적 체커는 "및 ED"계약을 나누면 더 잘 작동합니다. 따라서 코드를 변경하면 다음과 같습니다.

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 Contracts Checker 도구에 대해서는 잘 모르지만 범위 분석은 표준 정적 분석 기술입니다. 상업용 정적 분석 도구에 널리 사용되어 첨자 표현이 합법적인지 확인합니다.

MS Research는 이러한 종류의 정적 분석에서 좋은 실적을 보유하고 있으므로 현재 확인되지 않았지만 계약 검사기의 목표가 될 것으로 예상됩니다.