Contratti di codice: è necessario specificare le dichiarazioni di Contract.Requires (...) in modo ridondante nei metodi di delega?

Question

Ho intenzione di utilizzare la nuova funzionalità .NET 4 Contratti di codice per lo sviluppo futuro. Questo mi ha fatto chiedere se dobbiamo specificare equivalenti dichiarazioni Contract.Requires(...) in una catena di metodi ridondante.

Credo che un esempio di codice vale più di mille parole:

public bool CrushGodzilla(string weapon, int velocity) 
    { 
     Contract.Requires(weapon != null); 

     // long code 

     return false; 
    } 

    public bool CrushGodzilla(string weapon) 
    { 
     Contract.Requires(weapon != null); // specify contract requirement here 
              // as well??? 

     return this.CrushGodzilla(weapon, int.MaxValue); 
    } 

per la verifica runtime non importa molto, come avremo modo di fine sempre colpito il controllo requisito, e noi ci metteremo un errore se fallisce.

Tuttavia, è considerato una cattiva pratica quando non si specifica nuovamente il requisito del contratto nel secondo sovraccarico?

Inoltre, ci sarà la caratteristica di momento della compilazione controllo, ed eventualmente anche fase di progettazione il controllo dei contratti di codice. Sembra che non sia ancora disponibile per C# in Visual Studio 2010, ma penso che ci siano alcune lingue come SpeC# che già fanno. Questi motori probabilmente ci daranno suggerimenti quando scriviamo il codice per chiamare un tale metodo e il nostro argomento al momento può essere o sarà null.

Quindi mi chiedo se questi motori analizzeranno sempre uno stack di chiamate finché non troveranno un metodo con un contratto che al momento non è soddisfatto?

Inoltre, here I learned about the difference between Contract.Requires(...) and Contract.Assume(...). Suppongo che la differenza sia anche quella di considerare nel contesto di questa domanda?

Answer 1

Penso che sarebbe la migliore prassi per specificare tutti i contratti su ciascuno dei metodi pubblici. Un contratto è più che "ciò che viene controllato" - anche la documentazione è efficace. Se chiami un metodo ma non sai quale contratto viene applicato, sarebbe dispari ottenere un errore del contratto più in basso: ciò suggerirebbe un bug nel metodo che stai chiamando, piuttosto che nel metodo .

Si noti che se si utilizza C# 4 in tutto il progetto, è possibile prendere in considerazione l'utilizzo di parametri facoltativi e argomenti con nome per evitare di avere così tanti sovraccarichi. Questo non è utile se hai bisogno di chiamare il codice da una lingua che non li supporta, ovviamente.

ho il forte sospetto che, se non si specifica il contratto nel "inadempiente" sovraccarico, il correttore statica (che è ora available for all versions of VS2010) si lamentano che il contratto potrebbe non riuscire, e sarà anche suggerire aggiungendo il contratto in questione.

Answer 2

inoltre, ci sarà la caratteristica di momento della compilazione controllo, e forse anche fase di progettazione il controllo di codice contratti. Sembra che non è ancora disponibile per C# in Visual Studio 2010 ...

E 'disponibile, ma per farlo funzionare bisogna essere utilizzando VS2010 Ultimate Edition.

Avviso: Questo è un po 'speculativo, ma sembra essere corretto da quello che ho imparato ad usarlo;

È necessario propagare manualmente i vincoli tramite i metodi, come si è fatto.

L'unica informazione che i Contratti di codice possono vedere dall'esterno di un metodo è ciò che viene detto. Può esaminare ipotesi e asserzioni all'interno di un metodo, ma questa analisi non si propaga. In altre parole, CC non può "vedere attraverso" i tuoi metodi, quindi non sa automaticamente che CrushGodzilla(string) richiederà che il valore weapon non sia nullo.

Se si utilizza l'analisi statica, esso deve svolgere controlli in CrushGodzilla(string) e rendersi conto che weapon non può essere nullo, utilizzando il esterna informazioni su CrushGodzilla(string,int), e suggerirà che si aggiunge una precondizione non nullo Requires. (La non propagazione è il fatto che questa conoscenza non verrà utilizzata per analizzare il resto del programma.)

Non ho mai trovato da nessuna parte che documenti l'analizzatore statico molto bene, nonostante abbia guardato.