¿Cómo puedo especificar contratos de código para el código de marco existente (BCL)?

Question

Los contratos de código funcionan muy bien hasta que tenga que agregar un bazillion Contract.Assume(...) para los resultados que salen del código de la estructura. Por ejemplo, MemoryStream.ToArray() nunca devuelve una matriz nula, lo mejor que puedo ver al mirarlo en Reflector, pero no está documentado como un contrato, por lo que tengo que Assume en todas partes.

¿Existe alguna forma mágica de crear una biblioteca de contratos para las funciones que ya existen? Supongo que una vez que haya contratado unas pocas docenas de las funciones de marco más utilizadas, las advertencias serán mucho más aceptables.

Answer 1

No creo que puedas directamente. Hay varias cosas que hacer:

Solicite que se agregue el contrato en this thread en los foros de Code Contracts.

La solución sugerida por el equipo de Contratos de código por ahora es hacer un método estático que asuma todos los contratos que necesita. Me parece que esto funciona mejor con un método de extensión:

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

De esta manera, se utiliza s.ToArrayContracted() en lugar de s.ToArray(), y una vez que los contratos son disponibles en el tipo, sólo puede buscar y reemplazar ToArrayContracted a ToArray.