tempo de compilação check-in Design by Contract?

Question

Eu li que compilador pode impor DBC em tempo de compilação .. Como ele faz isso?

Answer 1

Tanto quanto eu sei, o mais poderoso estática linguagem DbC até agora é Spec # pela Microsoft Research . Ele usa uma ferramenta de análise estática poderosa chamada Boogie que por sua vez usa um poderoso Theorem Prover / restrição Solver chamado < a href = "http://Research.Microsoft.Com/projects/z3/" rel = "noreferrer"> Z3 para provar quer o cumprimento ou a violação de contratos em tempo de design.

Se o Teorema Prover pode provar que um contrato será sempre ser violada, isso é um erro de compilação. Se o Teorema Prover pode provar que um contrato será não ser violada, isso é uma otimização:. Os cheques contrato são removidos da DLL final

Como Charlie Martin aponta, provando contratos em geral é equivalente a resolver a detenção problema e, portanto, não é possível. Assim, haverá um monte de casos, onde o Teorema Prover pode provar nem refutar o contrato. Nesse caso, uma verificação de tempo de execução é emitida, assim como em outros sistemas de contratos, menos poderosos.

Por favor note que Spec # não está mais sendo desenvolvido. O motor de contrato foi extraído em uma biblioteca, chamada contratos de código para .NET , que será uma parte de .NET 4.0 / Visual Studio 2010. no entanto, não haverá suporte ao idioma para os contratos.

Answer 2

O compilador pode usar estática análise para olhar para o seu programa e determinar se ele faz o coisa certa. Como um exemplo simples, o seguinte código pode tentar tirar a raiz quadrada de um número negativo (C ++):

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

Se o compilador sabe que sqrt nunca deve ser chamado com um número negativo, que poderia marcar isto como um problema, porque ele sabe que a leitura da entrada do usuário pode retornar um número negativo. Por outro lado, se você fizer isso:

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

então o compilador pode dizer que esse código nunca vai chamar sqrt com um número negativo.

Answer 3

Design by Contract é um termo muito abstrato, já que pode haver muitos formalismos de especificação com diferentes poderes de expressão. Além disso, não existe actualmente um limite para as habilidades de análise estática para verificar e fazer cumprir as especificações. É um dos mais campos de pesquisa acadêmica e industrial ativos em ciência da computação.

Na prática, é provável que você vai usar algum subconjunto de contratos e verificação, e que depende do idioma que você está usando e sobre os plugins ou programas que você instala.

Em geral, as tentativas de análise estática para construir um modelo do contrato, e um modelo do programa atual, e compará-los. Por exemplo, se o contrato não permite que você chamar uma função quando um objeto está em estado de S, ela tentará determinar se em qualquer seqüência de invocação você pode acabar no estado S.

Answer 4

Qual compilador e que língua? Eiffel pode fazê-lo até certo ponto. Mas lembre-se que completamente impor projeto-por-contrato significaria ser capaz de resolver o Deter Problem (prova: suponha que você tenha um compilador que poderia fazê-lo Em seguida, o compilador teria que ser capaz de identificar uma função arbitrária com uma condição de saída verdade. que não pode alcançar o estado de saída devido a um ciclo infinito ou recursão infinito. Assim, reduz-se a suspensão.)

O que é geralmente entende por isso é que se você tiver uma chamada

  foo(a);

e em outro lugar definir

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

então o compilador pode verificar que um é, na verdade, vai ser no intervalo aberto (0..128).

Answer 5

Algumas linguagens como D ter sido razoavelmente poderoso dobrar compilação constante de tempo e de compilação condição de verificação de tempo (por D static assert(boolCond, msg);, IIRC C / C ++ pode usar #if e pragma ou #error)