Come è possibile specificare i contratti di codice per il codice del framework esistente (BCL)?

Question

I contratti di codice funzionano benissimo finché non è necessario aggiungere un miliardo di Contract.Assume(...) per i risultati che escono dal codice quadro. Ad esempio, MemoryStream.ToArray() non restituisce mai un array nullo, come meglio posso dire dall'osservarlo in Reflector, ma non è documentato come un contratto, quindi devo spostarlo dappertutto su Assume.

Esiste un modo magico per creare una biblioteca di contratti per funzioni già esistenti? Immagino che una volta che alcune dozzine delle funzioni di framework più comunemente utilizzate siano state ridotte, gli avvertimenti sarebbero diventati molto più appetibili.

Answer 1

Non penso che tu possa direttamente. Ci sono diverse cose da fare:

Richiedere l'aggiunta del contratto in this thread sui forum dei Contratti di Codice.

Il workaround suggerito dal team di Contratti di codice per ora è di creare un metodo statico che presupponga tutti i contratti necessari. Trovo che questo funziona meglio con un metodo di estensione:

static class Contracted 
{ 
    byte[] ToArrayContracted(this MemoryStream s) 
    { 
     Contract.Requires(s != null); 
     Contract.Ensures(Contract.Result<byte[]>() != null); 

     var result = s.ToArray(); 
     Contract.Assume(result != null); 
     return result; 
    } 
} 

In questo modo, è possibile utilizzare s.ToArrayContracted() invece di s.ToArray(), e una volta che i contratti sono disponibili sul tipo, si può solo cercare e sostituzione ToArrayContracted a ToArray.