Czy sprawdzanie statyczne Code Contracts może sprawdzać powiązanie arytmetyczne?

Question

(Również posted on the MSDN forum - ale to nie dostać dużo ruchu, o ile mogę zobaczyć.)

Próbowałem dostarczyć przykład Assert i Assume. Oto kod mam:

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; 
} 

(Segment o byciu w stanie przejść w null odniesienia zamiast istniejącego Random odniesienia jest czysto pedagogicznej, oczywiście.)

Miałem nadzieję, że jeśli kontroler wiedział, że każdy z nich w zakresie [1, 6] był w stanie obliczyć, że suma była w zakresie [2, 12].

Czy to nieracjonalna nadzieja? Rozumiem, że to trudny biznes, dokładnie to, co może się wydarzyć, ale miałem nadzieję, że kontroler będzie wystarczająco sprytny :)

Jeśli to nie jest teraz obsługiwane, czy ktoś tutaj wie, czy prawdopodobnie będzie obsługiwane w najbliższą przyszłość?

EDYCJA: Odkryłem, że są bardzo skomplikowane opcje arytmetyczne w statycznym sprawdzeniu. Korzystając z "zaawansowanego" pola tekstowego, mogę je wypróbować z Visual Studio, ale nie da się wytłumaczyć tego, co robią, o ile wiem.

Answer 1

Otrzymałem odpowiedź na forum MSDN. Okazuje się, że byłem już prawie na miejscu. Zasadniczo sprawdzanie statyczne działa lepiej, jeśli dzielisz kontrakty "and-ed". Tak więc, jeśli zmienimy kod na:

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; 
} 

To działa bez żadnych problemów. Oznacza to również, że przykład jest jeszcze bardziej użyteczny, ponieważ podkreśla to, że kontroler działa lepiej w przypadku oddzielnych umów.

Answer 2

Nie wiem o narzędziu MS Contracts Checker, ale analiza zakresu jest standardową techniką analizy statycznej; jest szeroko stosowany w komercyjnych narzędziach analizy statycznej do sprawdzenia, czy wyrazy w indeksie dolnym są legalne.

MS Research ma dobre osiągnięcia w tego rodzaju analizie statycznej, więc spodziewam się, że taka analiza zakresu będzie celem sprawdzania kontraktów, nawet jeśli nie jest obecnie sprawdzana.