Il controllore statico dei contratti con codice può controllare il limite aritmetico?

Question

(anche posted on the MSDN forum - ma questo non ottiene molto traffico, per quanto posso vedere.)

ho cercato di fornire un esempio di Assert e Assume. Ecco il codice che ho:

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

(Il business di essere in grado di passare in un riferimento null invece di un Random riferimento esistente è puramente pedagogica, naturalmente.)

avevo sperato che se il correttore sapeva che firstRoll e secondRoll erano ciascuno nell'intervallo [1, 6], sarebbe stato in grado di calcolare che la somma era nell'intervallo [2, 12].

È una speranza irragionevole? Mi rendo conto che è un affare complicato, che funziona esattamente cosa potrebbe accadere ... ma speravo che il correttore sarebbe stato abbastanza furbo :)

Se questo non è supportato ora, qualcuno sa se è probabile che sia supportato nel prossimo futuro?

EDIT: Ho trovato ora che ci sono opzioni molto complicate per l'aritmetica nel correttore statico. Usando la casella di testo "avanzata" posso provarli da Visual Studio, ma non c'è una spiegazione decente di quello che fanno, per quanto posso dire.

Answer 1

Ho avuto una risposta sul forum MSDN. Si scopre che ero quasi lì. Fondamentalmente il controllo statico funziona meglio se dividi i contratti "ed-ed". Quindi, se cambiamo il codice a questo:

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

Che funziona senza problemi. Significa anche che l'esempio è ancora più utile, in quanto mette in evidenza il punto che il correttore fa funziona meglio con contratti separati.

Answer 2

Non conosco lo strumento MS Contracts Checker, ma l'analisi di intervallo è una tecnica di analisi statica standard; è ampiamente utilizzato negli strumenti di analisi statica commerciale per verificare che le espressioni di pedici siano legali.

MS Research ha una buona esperienza in questo tipo di analisi statica, e quindi mi aspetterei che l'analisi di tale intervallo fosse un obiettivo del Controllore dei contratti, anche se non attualmente controllato.