Eu tenho lido alguns artigos sobre tipos dependentes e contratos de programação. Da maior parte do que li, parece que os contratos são verificados dinamicamente e os tipos dependentes são estaticamente verificados.
Houve alguns documentos que me fizeram pensar que é possível ter contratos parcialmente verificados estaticamente:
Em um nível prático, contratos são afirmações. Eles permitem verificar propriedades (sem quantificadores) de execuções individuais de um programa. A idéia principal no coração da verificação do contrato é a idéia da culpa - basicamente, você quer saber quem é o culpado por uma violação do contrato. Pode ser uma implementação (que não calcula o valor prometido) ou o chamador (que passou uma função com o tipo errado de valor).
O principal insight é que você pode rastrear a culpa usando o mesmo mecanismo que os pares de incorporação-projeção na construção de limites inversos da teoria de domínio. Basicamente, você muda de trabalhar com asserções para trabalhar com pares de asserções, uma das quais culpa o contexto do programa e a outra culpa do programa. Isso permite agrupar funções de ordem superior com contratos, porque é possível modelar a contravariância do espaço de função trocando o par de asserções. (Veja o artigo de Nick Benton "Desfazendo a digitação dinâmica" , por exemplo.)
Tipos dependentes são tipos. Os tipos especificam regras para afirmar se determinados programas são aceitáveis ou não. Como resultado, eles não incluem coisas como a noção de culpa, pois sua função é impedir que programas mal comportados existam em primeiro lugar. Não há nada para culpar, uma vez que apenas programas bem formados são até expressões gramaticais. Pragmaticamente, isso significa que é muito fácil usar tipos dependentes para falar de propriedades de termos com quantificadores (por exemplo, que uma função funciona para todas as entradas).
Essas duas visões não são as mesmas, mas estão relacionadas. Basicamente, o ponto é que, com contratos, começamos com um domínio universal de valores e usamos contratos para reduzir as coisas. Mas quando usamos tipos, tentamos especificar domínios menores de valores (com uma propriedade desejada) antecipadamente. Assim, podemos conectar os dois por meio de famílias de relações direcionadas ao tipo (ou seja, relações lógicas). Por exemplo, veja a recente "culpa por todos" de Ahmed, Findler, Siek e Wadler , ou "O significado dos tipos de Reynolds : da intrínseca à semântica extrínseca" .
Por que você diz que os contratos são livres de quantificadores?
Radu GRIGore #
3
Como você geralmente não pode usar testes para estabelecer propriedades de funções universalmente quantificadas, isso é tudo.
Neel Krishnaswami
3
A menos que os quantificadores abranjam domínios finitos, nesse caso, eles podem ser vistos como grandes conjunções e disjunções. Ou, se você quiser ser extravagante, pode verificar certos tipos de declarações quantificadas, desde que os quantiers abranjam os tipos pesquisáveis de Martin Escardo (que podem ser infinitos).
Andrej Bauer
2
@ Radu: Eu chamo coisas como JML & co "program logics". Os idiomas de asserção das lógicas dos programas não se restringem a termos do idioma dos programas. Isso permite descartar coisas como afirmações não determinantes ou com efeitos colaterais, que não têm uma boa interpretação lógica. (No entanto, essas coisas importam para verificação de contrato - ver o trabalho recente de Pucella e Tove a ESOP sobre o uso, contratos imperativas stateful para rastrear propriedades de linearidade.)
O problema (bastante abstrato) que tipos e contratos atacam é "Como garantir que os programas tenham certas propriedades?". Existe aqui uma tensão inerente entre poder expressar uma classe mais ampla de propriedades e verificar se um programa tem ou não uma propriedade. Os sistemas de tipos geralmente garantem uma propriedade muito específica (o programa nunca falha de certas maneiras) e possuem um algoritmo de verificação de tipos. Por outro lado, os contratos permitem especificar uma gama muito ampla de propriedades (por exemplo, a saída deste programa é um número primo), mas não vêm com um algoritmo de verificação.
No entanto, o fato de não haver algoritmo de verificação de contrato (que sempre funciona) não significa que não haja quase algoritmos de verificação de contrato (que tendem a funcionar na prática). Eu recomendaria que você olhasse o Spec # e o plugin Jessie do Frama-C . Ambos trabalham expressando "este programa obedece a este contrato" como uma declaração na lógica de primeira ordem via geração de condição de verificação e, em seguida, solicitando a um SMTsolver ir tentar encontrar uma prova. Se o solucionador falhar em encontrar uma prova, o programa está errado ou, bem, o solucionador falhou em encontrar uma prova que exista. (É por isso que esse é um algoritmo "quase" de verificação de contratos.) Também existem ferramentas baseadas na execução simbólica, o que significa aproximadamente que "este programa obedece a esse contrato" é expresso como um monte de proposições (em alguma lógica). Veja, por exemplo, jStar .
O trabalho de Flanagan tenta tirar o melhor dos dois mundos, de modo que você possa verificar rapidamente as propriedades do tipo e depois trabalhar pelo resto. Eu não estou realmente familiarizado com os tipos híbridos, mas lembro-me do autor dizendo que sua motivação era encontrar uma solução que requer menos anotações (do que seu trabalho anterior em ESC / Java). Em certo sentido, no entanto, também existe uma integração frouxa entre tipos e contratos no ESC / Java (e número da especificação): ao verificar contratos, o solucionador é informado de que a verificação de tipo foi bem-sucedida para que ela pudesse ver essas informações.
Os contratos podem ser verificados estaticamente. Se você olhar para o antigo trabalho de Dana Xu sobre ESC / Haskell , ela foi capaz de implementar a verificação de contrato completa em tempo de compilação, contando apenas com um provador de teoremas de aritmética. A rescisão é resolvida por um simples limite de profundidade, se bem me lembro:
Tanto os contratos quanto os tipos permitem representar especificações no estilo Hoare (condição pré / pós) nas funções. Ambos podem ser verificados estaticamente no tempo de compilação ou dinamicamente no tempo de execução.
Tipos dependentes permitem codificar uma gama muito ampla de propriedades no sistema de tipos, os tipos de propriedades que os programadores contratados esperam. Isso ocorre porque eles podem depender dos valores do tipo. Os tipos dependentes tendem a ser verificados estaticamente, embora eu acredite que os artigos que você citou examinem abordagens alternativas.
Em última análise, há pouca diferença. Eu acho que os tipos dependentes são uma lógica na qual você pode expressar especificações, enquanto os contratos são uma metodologia de programação na qual você expressa especificações.
É um pouco enganador dizer que as anotações no estilo Hoare podem ser verificadas estaticamente. Se a lógica é FO, como geralmente é, então o problema é certamente indecidível. Mas, sim, eu sei que você quis dizer que é possível tentar e até ter sucesso em muitas situações.
Radu GRIGore
1
Fiquei com a impressão de que gerar a prova pode ser indecidível, mas verificar uma prova deve ser. Muitas linguagens de tipo dependente dependem do usuário para fornecer o valor de prova da habitação do tipo de teorema.
Jason Reich #
Você está certo. Mas eu moro no mundo automatizado, onde o usuário geralmente não precisa de uma prova.
O problema (bastante abstrato) que tipos e contratos atacam é "Como garantir que os programas tenham certas propriedades?". Existe aqui uma tensão inerente entre poder expressar uma classe mais ampla de propriedades e verificar se um programa tem ou não uma propriedade. Os sistemas de tipos geralmente garantem uma propriedade muito específica (o programa nunca falha de certas maneiras) e possuem um algoritmo de verificação de tipos. Por outro lado, os contratos permitem especificar uma gama muito ampla de propriedades (por exemplo, a saída deste programa é um número primo), mas não vêm com um algoritmo de verificação.
No entanto, o fato de não haver algoritmo de verificação de contrato (que sempre funciona) não significa que não haja quase algoritmos de verificação de contrato (que tendem a funcionar na prática). Eu recomendaria que você olhasse o Spec # e o plugin Jessie do Frama-C . Ambos trabalham expressando "este programa obedece a este contrato" como uma declaração na lógica de primeira ordem via geração de condição de verificação e, em seguida, solicitando a um SMTsolver ir tentar encontrar uma prova. Se o solucionador falhar em encontrar uma prova, o programa está errado ou, bem, o solucionador falhou em encontrar uma prova que exista. (É por isso que esse é um algoritmo "quase" de verificação de contratos.) Também existem ferramentas baseadas na execução simbólica, o que significa aproximadamente que "este programa obedece a esse contrato" é expresso como um monte de proposições (em alguma lógica). Veja, por exemplo, jStar .
O trabalho de Flanagan tenta tirar o melhor dos dois mundos, de modo que você possa verificar rapidamente as propriedades do tipo e depois trabalhar pelo resto. Eu não estou realmente familiarizado com os tipos híbridos, mas lembro-me do autor dizendo que sua motivação era encontrar uma solução que requer menos anotações (do que seu trabalho anterior em ESC / Java). Em certo sentido, no entanto, também existe uma integração frouxa entre tipos e contratos no ESC / Java (e número da especificação): ao verificar contratos, o solucionador é informado de que a verificação de tipo foi bem-sucedida para que ela pudesse ver essas informações.
fonte
Os contratos podem ser verificados estaticamente. Se você olhar para o antigo trabalho de Dana Xu sobre ESC / Haskell , ela foi capaz de implementar a verificação de contrato completa em tempo de compilação, contando apenas com um provador de teoremas de aritmética. A rescisão é resolvida por um simples limite de profundidade, se bem me lembro:
fonte
Tanto os contratos quanto os tipos permitem representar especificações no estilo Hoare (condição pré / pós) nas funções. Ambos podem ser verificados estaticamente no tempo de compilação ou dinamicamente no tempo de execução.
Tipos dependentes permitem codificar uma gama muito ampla de propriedades no sistema de tipos, os tipos de propriedades que os programadores contratados esperam. Isso ocorre porque eles podem depender dos valores do tipo. Os tipos dependentes tendem a ser verificados estaticamente, embora eu acredite que os artigos que você citou examinem abordagens alternativas.
Em última análise, há pouca diferença. Eu acho que os tipos dependentes são uma lógica na qual você pode expressar especificações, enquanto os contratos são uma metodologia de programação na qual você expressa especificações.
fonte