reservadas - Contratos de código C#: ¿Qué puede probarse estáticamente y qué no?

palabras reservadas en programacion y su significado

Question

Podría decir que me estoy familiarizando con los contratos de código: he leído y comprendido la mayor parte del manual del usuario y los he estado usando durante bastante tiempo, pero todavía tengo preguntas. Cuando busco SO para ''códigos de contrato no comprobados'' hay bastantes resultados, todos preguntando por qué su declaración específica no pudo ser probada estáticamente. Aunque podría hacer lo mismo y publicar mi escenario específico (que es por cierto:

)

Prefiero entender por qué cualquier condición de Contrato del Código puede o no puede ser probada. A veces estoy impresionado con lo que puede probar, y otras veces estoy ... bueno ... para decirlo cortésmente: definitivamente no estoy impresionado. Si quiero entender esto, me gustaría conocer los mecanismos que usa el verificador estático. Estoy seguro de que aprenderé por experiencia, pero estoy fumigando el Contract.Assume Asume las declaraciones por todo el lugar para hacer que desaparezcan las advertencias, y creo que no es para eso que están destinados los Contratos de Código. Google no me ayudó, así que quiero preguntarles por sus experiencias: ¿qué patrones (no obvios) han visto? ¿Y qué te hizo ver la luz?

Answer 1

El contrato en su construcción no se cumple. Ya que está haciendo referencia al campo de un objeto (this.data), otros subprocesos pueden tener acceso al campo y pueden cambiar su valor entre la Asunción y la resolución del primer parámetro y la resolución del tercer parámetro. (ei, podrían ser tres matrices completamente diferentes).

Debe asignar la matriz a una variable local, luego usar esa variable en todo el método. Entonces el analizador sabrá que se están cumpliendo las restricciones, porque ningún otro subproceso tendrá la capacidad de cambiar la referencia.

var localData = this.data;
if (localData == null) return;
byte[] newData = new byte[localData.Length]; // Or whatever the datatype is.
Array.Copy(localData, newData, localData.Length); // Now, this cannot fail.

Esto tiene el beneficio adicional de no solo satisfacer la restricción, sino que, en realidad, hace que el código sea más robusto en muchos casos.

Espero que esto te lleve a la respuesta a tu pregunta. Realmente no pude responder a su pregunta directamente, porque no tengo acceso a una versión de Visual Studio que incluye el verificador estático. (Estoy en VS2008 Pro). Mi respuesta se basa en lo que mi propia inspección visual del código concluiría, y parece que el comprobador de contrato estático utiliza técnicas similares. Estoy intreagued! Necesito conseguirme uno de ellos. :-RE

ACTUALIZACIÓN: (Mucha especulación a seguir)

Después de reflexionar, creo que puedo hacer una buena suposición de lo que puede o no puede probarse (incluso sin acceso al comprobador estático). Como se indica en la otra respuesta, el verificador estático no realiza un análisis interprocedente. Por lo tanto, con la posibilidad inminente de accesos de variables de múltiples subprocesos (como en el OP), el verificador estático solo puede tratar con eficacia las variables locales (como se define a continuación).

Por "variables locales" me refiero a una variable a la que ningún otro hilo puede acceder. Esto incluiría cualquier variable declarada en el método o pasada como parámetro, a menos que el parámetro esté decorado con ref o out o la variable se capture en un método anónimo.

Si una variable local es un tipo de valor, entonces sus campos también son variables locales (y así sucesivamente).

Si una variable local es un tipo de referencia, solo la referencia en sí, no sus campos, puede considerarse una variable local. Esto es cierto incluso para un objeto construido dentro del método, ya que un constructor en sí puede filtrar una referencia al objeto construido (por ejemplo, a una colección estática para almacenamiento en caché).

Mientras el verificador estático no realice ningún análisis interprocedente, cualquier suposición que se haga sobre las variables que no son locales como se definió anteriormente se puede invalidar en cualquier momento y, por lo tanto, se ignoran en el análisis estático.

Excepción 1: dado que el tiempo de ejecución sabe que las cadenas y los arrays son inmutables, sus propiedades (como Length) están sujetas a análisis, siempre que la cadena o la variable del array sea local. Esto no incluye los contenidos de una matriz que son mutables por otros subprocesos.

Excepción 2: el tiempo de ejecución puede saber que el constructor de la matriz no pierde ninguna referencia a la matriz construida. Por lo tanto, una matriz que se construye dentro del cuerpo del método y no se filtra fuera del método (que se pasa como un parámetro a otro método, se asigna a una variable no local, etc.) tiene elementos que también pueden considerarse variables locales.

Estas restricciones parecen bastante onerosas, y puedo imaginar varias formas en que esto podría mejorarse, pero no sé qué se ha hecho. Aquí hay algunas otras cosas que, en teoría, podrían hacerse con el verificador estático. Alguien que lo tenga a la mano debería verificar qué se ha hecho y qué no:

• Podría determinar si un constructor no filtra ninguna referencia al objeto o sus campos y considera que los campos de cualquier objeto así construido son variables locales.
• Se podría realizar un análisis de no fugas en otros métodos para determinar si un tipo de referencia pasado a un método todavía puede considerarse local después de esa invocación del método.
• Las variables decoradas con ThreadStatic o ThreadLocal pueden considerarse variables locales.
• Se podrían dar opciones para ignorar la posibilidad de usar la reflexión para modificar valores. Esto permitiría que los campos de solo lectura privados en los tipos de referencia o los campos de solo lectura privados estáticos se consideren inmutables. Además, cuando esta opción está habilitada, una variable privada o interna X a la que solo se accede dentro de una construcción de lock(X){ /**/ } y que no se ha filtrado podría considerarse una variable local. Sin embargo, estas cosas, en efecto, reducirían la confiabilidad del verificador estático, por lo que es un poco dudoso.

Otra posibilidad que podría abrir una gran cantidad de nuevos análisis sería la asignación declarativa de variables y los métodos que los utilizan (y así sucesivamente) a un hilo único en particular. Esto sería una adición importante al lenguaje, pero podría valer la pena.

Answer 2

La respuesta corta es que el analizador de código estático parece ser muy limitado. Por ejemplo, no detecta

readonly string name = "I''m never null";

como siendo un invariante. Por lo que puedo reunir en los foros de MSDN, analiza cada método por sí mismo (por razones de rendimiento, no es que uno piense que podría ser mucho más lento), lo que limita su conocimiento al verificar el código.

Para lograr un equilibrio entre el alto objetivo académico de demostrar la corrección y poder realizar el trabajo, he recurrido a decorar métodos individuales (o incluso clases, según sea necesario) con

[ContractVerification(false)]

En lugar de esparcir la lógica con un montón de Supuestos. Puede que esta no sea la mejor práctica para usar CC, pero proporciona una manera de deshacerse de las advertencias sin desactivar ninguna de las opciones del verificador estático. Para no perder las verificaciones previas / posteriores a la condición de tales métodos, generalmente agrego un talón con las condiciones deseadas y luego invoco el método excluido para realizar el trabajo real.

Mi propia evaluación de los Contratos de Código es que es genial si solo está utilizando las bibliotecas de marcos oficiales y no tiene muchos códigos heredados (por ejemplo, cuando comienza un nuevo proyecto). Cualquier otra cosa y es una mezcla de placer y dolor.