Perché questo contratto di codice C# non è valido?

Question

Visual Studio mostra un errore quando scrivo questo contratto di seguito.

Errore 20 Sezione del contratto non valida nel metodo '....get_Page'

Il problema è con il blocco "se"?

public int? Page
{
get
{
    int? result = Contract.Result<int?>();

    if (result != null)
        Contract.Ensures(result >= 0);

    return default(int?);
}
}

MODIFICARE:

Lasse V.Karisen ha pubblicato nei commenti:

Che ne dite di:Contract.Ensures(risultato == null || risultato >= 0);?

Sì Karisen, l'ho già provato e si compila.Ma la domanda rimane:non è possibile avere se quando si utilizzano i contratti?

Un altro problema che sto riscontrando è senza tracce (soprattutto considerando che l'esempio sopra funziona), coinvolge anche l'uso di result:

public int IndexOf(T item)
{
    Contract.Assert(item != null);
    Contract.Assert((item as IEntity).ID > 0);

    int result = Contract.Result<int>();
    Contract.Ensures(result >= -1);

    return default(int);
}

Answer 1

Basta avere una supposizione. Forse dovrebbe essere Contract.Ensures(result.Value >= 0)?

Answer 2

Il contratto non è corretto, perché tutte le clausole contratto deve comparire prima di qualsiasi altro codice.

Answer 3

Non hai bisogno di un caso, per fare la manipolazione boolian utilizzare invece implica!

public int? Page
{
    get
    {
        Contract.Ensures( (result!= null).Implies(result >= 0) );
        var result = ...

        ...


        return result;
    }
}

Inoltre si dovrebbe usare richiede non valere quando si verifica argomenti del metodo, e di altri presupposti.

public int IndexOf(T item)
{
    Contract.Requires(item != null);
    Contract.Requires((item as IEntity).ID > 0);
...

Answer 4

Il contratto presenta un flag di compilazione condizionale.Nella versione più codice

if condition
    contract
return

diventa

if condition
   return

vedi il problema adesso?

Answer 5

Tutte le chiamate Guarantees e Requires devono essere prima di tutte le altre istruzioni nel corpo di un metodo o di una proprietà, questo include assegnazioni semplici come quelle che stai utilizzando che aiutano la leggibilità.

Sintassi corretta

public int? Page {
    get {
        Contract.Ensures(Contract.Result<int?>() == null 
            || Contract.Result<int?>() >= 0); 

        return default(int?);
        }
    }
 }

Questo è molto brutto, molto più brutto del normale if (x || y) throw new ArgumentOutOfRangeException().

Attributi speciali

C'è un modo un po' tortuoso per aggirare questo problema. ContractAbbreviatorAttribute E ContractArgumentValidatorAttribute sono attributi speciali che il ccrewrite capisce cosa ti semplifica la vita.(Per molti dettagli vedere il System.Diagnostics.Contracts documentazione dello spazio dei nomi su MSDN o sui contratti di codice Manuale.)

Se si utilizza .NET 4 o versioni precedenti:Questi attributi si trovano nel framework a partire da .NET 4.5, ma per le versioni precedenti è possibile ottenere un file di origine dalla directory in cui viene installato Code Contracts.(C:\Program Files (x86)\Microsoft\Contracts\Languages\) In quella cartella ci sono CSharp E VisualBasic sottocartelle che hanno un file ContractExtensions.cs (o .vb) contenente il codice richiesto.

ContractAbbreviatorAttributeQuesto attributo consente di creare effettivamente macro di contratto.Con esso, la proprietà della tua pagina potrebbe essere scritta in questo modo:

public int? Page {
    get {
        EnsuresNullOrPositive();
        return default(int?)
    }
}

[ContractAbbreviator]
static void EnsuresNullOrPositive(int? x) {
    Contract.Ensures(
        Contract.Result<int?>() == null ||                 
        Contract.Result<int?>() >= 0);
}

EnsuresNullOrPositive potrebbe anche essere mantenuto in una classe statica e riutilizzato nel progetto, oppure reso pubblico e inserito in una libreria di utilità.Potresti anche renderlo più generale come il prossimo esempio.

[ContractAbbreviator]
static void EnsuresNullOrPositive<Nullable<T>>(Nullable<T> obj) {
    Contract.Ensures(
        Contract.Result<Nullable<T>>() == null ||                 
        Contract.Result<Nullable<T>>() >= default(T));
}

Per la mia libreria di utilità, ho una classe statica denominata Requires e una classe statica denominata Ensures, ciascuno con molti metodi statici decorati con ContractAbbreviator.Ecco alcuni esempi:

public static class Requires {

    [ContractAbbreviator] 
    public static void NotNull(object obj) {  
        Contract.Requires<ArgumentNullException>(obj != null);
    }

    [ContractAbbreviator]
    public static void NotNullOrEmpty(string str) {
        Contract.Requires<ArgumentNullException>(!string.IsNullOrEmpty(str));
    }

    [ContractAbbreviator]
    public static void NotNullOrEmpty(IEnumerable<T> sequence) {
        Contract.Requires<ArgumentNullException>(sequence != null);
        Contract.Requires<ArgumentNullException>(sequence.Any());
    }
}

public static class Ensures {
    [ContractAbbreviator]
    public static void NotNull(){
        Contract.Ensures(Contract.Result<object>() != null);
    }
}

Questi possono essere usati in questo modo:

public List<SentMessage> EmailAllFriends(Person p) {
    Requires.NotNull(p); //check if object is null
    Requires.NotNullOrEmpty(p.EmailAddress); //check if string property is null or empty
    Requires.NotNullOrEmpty(p.Friends); //check if sequence property is null or empty
    Ensures.NotNull(); //result object will not be null

    //Do stuff
}

ContractArgumentValidatorAttributeNon l'ho usato al di fuori dei tutorial, ma fondamentalmente ti consente di scrivere diversi pacchetti if (test) throw new ArgumentException() chiamate in una singola chiamata che si comporta come una chiamata a Contract.Requires.Poiché si occupa solo della convalida degli argomenti, non sarebbe d'aiuto con il tuo esempio post-condizione.