An algebraic approach to the design of compilers for object-oriented languages

摘要

Neste trabalho discutimos o projeto de compiladores corretos por construção para linguagens orientadas a objeto. Um compilador correto é aquele que garante que a semântica é preservada quando o programa fonte _e traduzido para a linguagem destino. O projeto de compiladores corretos para linguagens imperativas se encontra bem fundamentado; atualmente, o maior desafio é o desenvolvimento de uma abordagem para lidar com características de orientação a objetos. Nesta tese, descrevemos uma abordagem algébrica para construção de compiladores corretos para uma linguagem orientada a objetos chamada ROOL (acrônimo para Refenement Objecy-oriented Language), que é similar a Java e C++. Esta linguagem inclue classes, herança, ligação dinâmica, recursão, cast e teste de tipos, e visibilidade baseada em classes. Na nossa abordagem, lidamos com o problema de corretude do compilador transformando a tarefa de compilação em uma tarefa de refinamento de programa. O processo de compilação passa ser identificado como sendo a redução de um programa fonte, escrito em um subconjunto executável da linguagem, para uma forma normal. A forma normal é gerada por uma série de transformações que preservam a corretude, e s ao provadas corretas a partir das leis básicas da linguagem; portanto o processo é correto por construção. A maior vantagem da nossa abordagem reside na caracterização do processo de compilação dentro de um sistema uniforme onde as comparações e traduções entre semânticas são evitadas. A redução a forma normal é formalizada como uma álgebra onde a noção central é a de refinamento de programas. Portanto, o produto da compilação é um programa na própria linguagem fonte. Nossa forma normal é um programa na forma de um interpretador, escrito na mesma linguagem fonte, emulando o comportamento da máquina destino. A partir desse interpretador, é que a seqüência das instruções geradas são capturadas. Definimos a Máquina Virtual de ROOL (RVM) como sendo nossa máquina destino; ela _e baseada na Máquina Virtual de Java (JVM) Tal uniformidade implica que todo o cálculo necessário para assegurar a corretude do processo de compilação é realizado em um único sistema de uma linguagem orientada a objetos cuja semântica é dada por leis algébricas. Nenhuma teoria relativa a linguagem fonte ou destino é desenvolvida ou usada no processo. O processo de compilação é justificado por teoremas de redução da forma normal. Existem cinco fases: pré-compilação de classes, redirecionamento de chamada de métodos, simplificação, eliminação de controle e refinamento de dados. Para cada fase, um teorema assegura o resultado esperado. O teorema principal conecta os passos intermediários e estabelece o resultado para todo o processo. Uma vez que os teoremas de redu¢c~ ao pra cada fase são provados corretos a partir das leis básicas de ROOL, eles corroboram para a corretude de todo o processo