Modelo formal de execução para Java (ou linguagem imperativa geral)

7

Estou tentando provar algumas declarações sobre a execução em programas Java sob algumas restrições pesadas (basicamente tenho uma conjectura de que, se dois métodos satisfazem um conjunto de restrições para uma determinada entrada, então eles são equivalentes - ou seja, que retornam valor e estado após execução são idênticas). Para provar isso, estou procurando algum tipo de formalismo que me permita falar sobre isso.

Eu estou familiarizado com a semântica operacional das linguagens funcionais e eu poderia traduzir loops / while loops para funções recursivas ... Prefiro não fazer isso e seria bom ter algumas máquinas para que eu pudesse permanecer em um território imperativo .

Mais especificamente, eu quero raciocinar sobre o estado de um método no k º passo da execução. Isso inclui o estado global:

  • Chamadas como this.field = 2atualizar nosso estado de classe
  • Chamadas que modificam parâmetros atualizam o estado fora do nosso método:
    • myParam.setFoo(...)
    • myParam.x = y
  • Chamadas para métodos estáticos
    • Blah.static_side_effects()

Estou assumindo que tudo isso é determinístico . Ou seja, quero formalizar a suposição de que, se alguma dessas atualizações globais do estado ocorrer em dois métodos, cujos estados de execução global e local são idênticos, o novo estado também será idêntico - que cada etapa da computação é determinada precisamente por estado global e estado local. Obviamente, isso impede RNGs e paralelismo (mas eu posso lidar com isso mais tarde ...).

Alguma idéia ou fonte de como eu poderia abordar isso? Meu único pensamento é tratar os métodos como uma lista de declarações e tentar descrever formalmente a semântica de uma declaração.

Se possível, eu adoraria fazer isso no nível da linguagem Java, e não no nível da JVM. Isso pode não ser viável, mas meu objetivo, no momento, é fazer algumas suposições razoáveis ​​sobre minha semântica operacional e, a partir daí, levá-la a partir daí.

Oh, uma observação final - todas as sugestões sobre como melhorar essa questão serão muito apreciadas. Estou meio que tentando encontrar o idioma certo para fazer a pergunta e se estou abusando da terminologia (como estado de execução local / global ...) adoraria corrigir isso.

Ben Kushigian
fonte
3
Talvez os artigos sobre "Featherweight Java" sejam relevantes. Já faz um tempo desde que li algo sobre isso, mas eles tentaram definir um subconjunto Java razoavelmente pequeno que ainda é suficientemente geral e admite uma semântica de tamanho decente. Fazer isso para Java completo é um exagero: a especificação oficial da linguagem é de 700 páginas de descrições informais, IIRC.
chi
Sim, dei uma olhada nas especificações e continuei. Além disso, essas são apenas as especificações de idioma IIR - as especificações da JVM têm outras 600-700 páginas. Mas vou olhar para o Java Featherweight. Obrigado pela sugestão
Ben Kushigian
Uau, Pierce e Wadler! Estarei lendo isso independentemente da sua aplicabilidade no meu trabalho: D
Ben Kushigian

Respostas:

7

O Java Featherweight é altamente considerado na comunidade PL. Mas se isso não atender às suas necessidades, aqui está uma abordagem geral à modelagem:

  • Formalize o AST do seu idioma em expressões e declarações
  • Escreva uma semântica para expressões e declarações. Sua semântica precisará de:
    • uma relação de avaliação, relacionando pares expressão-estado (e,σ) para uma expressão avaliada com estado atualizado (e,σ),
    • uma relação de execução, relacionando pares declaração-estado (s,σ) para estados de saída σ.
  • Eles serão recursivos entre si e podem ser uma semântica de grandes ou pequenos passos, dependendo da sua necessidade específica. O grande passo é mais simples, mas pior na modelagem de execuções que não terminam.

Essa estrutura básica o levará muito longe. Para modelar Java, você provavelmente deseja estruturar seu conjunto de estados hierarquicamente, em torno de objetos específicos, mas os princípios básicos são os mesmos. Você também deseja modelar o despacho dinâmico, portanto, provavelmente faz sentido transformar métodos de classe em funções, usando um argumento "this" explícito.

Uma semântica axiomática, ou seja, Hoare triplica, que define uma lógica de pré e pós-condições para declarações para modelar programas imperativos. Não sei como isso se relaciona com o POO, mas tenho certeza de que alguém tentou nos 50 anos em que esteve por aí.

Você pode também estar interessado em Fundamentos de Software . Ele é orientado a raciocinar sobre linguagens imperativas no provador do teorema de Coq, mas fornece uma excelente visão geral da semântica formal.

jmite
fonte
A semântica tripla / axiomática original da Hoare não lidava com construções de ordem superior, como objetos e funções de primeira classe. Abordagens mais modernas, como a lógica das implicações agrupadas, particularmente na forma de lógica de separação, e a teoria do tipo Hoare fornecem uma abordagem que pode lidar com esses recursos.
Derek Elkins saiu de SE
8

Existe uma semântica (operacional) para Java 1.4 formulada noKestrutura . Associado a essa estrutura, existe um sistema de prova chamado Matching Logic . Enquanto essa página descreve uma implementação de protótipo, parece que a funcionalidade está sendo incorporada aoKferramentas de estrutura em si kprover. Infelizmente, parece que a estrutura está no meio da atualização, e fazer com que a estrutura seja construída e funcione adequadamente é um pouco trabalhoso, e não tenho muita certeza de quão prática e / ou funcional kproveratualmente seja. No entanto, você pode provar manualmente as coisas referentes à semântica operacional (e também usar o sistema de prova da Matching Logic, se desejar). O documento que descreve a semântica Java, K-Java: uma semântica completa de Java , faz referência a outros sistemas que são menos completos, mas podem ser completos o suficiente para seus propósitos. Dito isto, eles podem não estar voltados para a comprovação de propriedades sobre programas Java. De fato, no artigo, a semântica está sendo usada para verificação de modelo, e não para provas de correção.

Essa é uma resposta se você deseja um alto grau de confiança de que o código Java real se comporta como você pretende. Se o objetivo é verificar mais o algoritmo do que a realização específica em Java, isso provavelmente é um exagero. Dito isto, você pode formalizar facilmente uma linguagem imperativa simplesKse você precisar apenas de recursos básicos imperativos / OO. De fato, isso é feito como um exercício noKtutorial de estrutura. De fato, se você puder reformular seu problema no fragmento de C suportado pelo protótipo da Matching Logic , poderá usá-lo como está.

Derek Elkins deixou o SE
fonte