¿Tiempo de compilación comprobando en Diseño por Contrato?

Question

Leí que el compilador puede imponer dbc en tiempo de compilación. ¿Cómo lo hace?

Answer 1

Por lo que sé, el lenguaje estático más poderoso de DbC hasta ahora es Spec # de Microsoft Research . Utiliza una poderosa herramienta de análisis estático llamada Boogie , que a su vez utiliza un poderoso Proyector de teoremas / Solucionador de restricciones llamado < a href = "http://Research.Microsoft.Com/projects/z3/" rel = "noreferrer"> Z3 para demostrar el cumplimiento o la violación de los contratos en el momento del diseño.

Si Theorem Prover puede probar que un contrato siempre se violará, es un error de compilación. Si Theorem Prover puede probar que un contrato nunca se violará, eso es una optimización: las verificaciones del contrato se eliminan de la DLL final.

Como señala Charlie Martin, probar los contratos en general equivale a resolver el problema de la detención y, por lo tanto, no es posible. Por lo tanto, habrá muchos casos en los que Theorem Prover no puede probar ni refutar el contrato. En ese caso, se emite una verificación de tiempo de ejecución, al igual que en otros sistemas de contratos menos potentes.

Tenga en cuenta que Spec # ya no se está desarrollando. El motor del contrato se ha extraído en una biblioteca, denominada Contratos de código para .NET , que formarán parte de .NET 4.0 / Visual Studio 2010. Sin embargo, no habrá soporte de idioma para los contratos.

Answer 2

El compilador puede usar análisis estático para ver su programa y determinar si lo hace. cosa correcta. Como un simple ejemplo, el siguiente código podría intentar tomar la raíz cuadrada de un número negativo (C ++):

double x;
cin >> x;
cout << sqrt(x) << endl;

Si el compilador sabe que sqrt nunca debe llamarse con un número negativo, podría marcar esto como un problema porque sabe que leer desde la entrada del usuario podría devolver un numero negativo. Por otro lado, si haces esto:

double x;
cin >> x;
if (x >= 0) {
    cout << sqrt(x) << endl;
} else {
    cout << "Can't take square root of negative number" << endl;
}

entonces el compilador puede decir que este código nunca llamará a sqrt con un número negativo.

Answer 3

Diseño por contrato es un término muy abstracto, ya que puede haber muchos formalismos de especificación con diferentes poderes de expresión. Además, en la actualidad existe un límite a las capacidades del análisis estático para verificar y hacer cumplir las especificaciones. Es uno de los campos de investigación académica e industrial más activos en informática.

En la práctica, es probable que utilice algún subconjunto de contratos y comprobaciones, y eso depende del idioma que esté utilizando y de los complementos o programas que instale.

En general, el análisis estático intenta construir un modelo del contrato y un modelo del programa real, y compararlos. Por ejemplo, si el contrato no le permite invocar una función cuando un objeto está en el estado S, intentará determinar si en alguna secuencia de invocación podría terminar en el estado S.

Answer 4

¿Qué compilador y qué idioma? Eiffel puede hacerlo hasta cierto punto. Pero recuerde que aplicar completamente el diseño por contrato significaría poder resolver el problema de detención (prueba: suponga que tiene un compilador que podría hacerlo. Entonces, el compilador tendría que poder identificar una función arbitraria con una condición de salida verdadera). eso no puede lograr la condición de salida debido a un bucle infinito o una recursión infinita. Por lo tanto, se reduce a detenerse.)

Lo que generalmente se entiende por esto es que si tienes una llamada

  foo(a);

y en otro lugar define

  function foo(a:int) is
     assert 0 < a && a < 128
     ...
  end

entonces el compilador puede verificar que a, de hecho, va a estar en el intervalo abierto (0..128).

Answer 5

Algunos lenguajes como D tienen un plegado constante de tiempo de compilación razonablemente potente y una verificación de la condición de tiempo de compilación (para D static asert (boolCond, msg); , IIRC C / C ++ puede usar #if y pragma o #error )