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

AUTOR(ES)
DATA DE PUBLICAÇÃO

2005

RESUMO

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 à 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 as 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 Renement Object-oriented Language), que à similar a Java e C++. Esta linguagem inclui 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Ão 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 e formalizada como uma Ãlgebra onde a noÃÃo central à a de refinamento de programas. Portanto, o produto da compilaÃÃo e 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 capturamos a seqÃÃncia das instruÃÃes geradas. Definimos a Maquina Virtual de ROOL (RVM) como sendo nossa mÃquina destino; ela à 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 e realizado em um Ãnico sistema de uma linguagem orientada a objetos cuja semÃntica à dada por leis algÃbricas. Nenhuma teoria relativa à linguagem fonte ou destino à desenvolvida ou usada no processo. O processo de compilaÃÃo à justificado por teoremas de reduÃÃo a forma normal. Existem cinco fases: pre-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ÃÃo para cada fase sÃo provados corretos a partir das leis bÃsicas de ROOL, eles corroboram para a corretude de todo o processo

ASSUNTO(S)

cÃlculo de refinamento linguagem da programaÃÃo ciencia da computacao rool

ACESSO AO ARTIGO

Documentos Relacionados