Defesa de Dissertação de Mestrado: André Willik Valenti
Document Actions
Defesa de Dissertação de Mestrado: Glauber Módolo Cabral
Criação de uma biblioteca padrão para a linguagem HasCASL.
| What | Defesa de Mestrado |
|---|---|
| When |
26/04/2010 from 10:00 to 12:00 |
| Where | Auditório do IC - Sala 85 - IC 2 |
| Add event to calendar |
vCal
iCal
|
Métodos formais podem ser usados como ferramentas da engenharia de software que empregam formalismos matemáticos na construção de programas.
Em geral, são compostos por uma ou mais linguagens de especificação e algumas ferramentas auxiliares.
A linguagem de especificação algébrica Common Algebraic Specification Language (CASL) foi concebida para ser a linguagem padrão na área de especificação algébrica.
Com suas características extraídas de outras linguagens, CASL foi projetada para possuir extensões e sublinguagens, além de permitir o suporte a novos paradigmas de programação.
A linguagem HasCASL, extensão responsável por suportar lógica de segunda ordem, possui um subconjunto de sua sintaxe que se assemelha à linguagem de programação Haskell e que pode, inclusive, ser executado.
O uso prático de uma linguagem de especificação depende da disponibilidade de uma biblioteca padrão de especificações pré-definidas.
CASL possui tal biblioteca e suas especificações podem ser importadas por especificações desenvolvidas em HasCASL.
No entanto, a biblioteca da linguagem CASL não disponibiliza propriedades e tipos de dados de segunda ordem.
Nesta dissertação, descreve-se a especificação de uma biblioteca para a linguagem HasCASL tendo como referência a biblioteca da linguagem Haskell.
A biblioteca criada provê funções e tipos de dados de segunda ordem, especificando tipos de dados e funções existentes em Haskell, tais como os tipos booleano, listas, caracteres e cadeias de caracteres.
Sua especificação utilizou tipos com avaliação estrita, devido à complexidade de iniciar-se as especificações com o uso de tipos com avaliação preguiçosa.
Uma segunda versão da biblioteca foi refinada para suportar tipos com avaliação preguiçosa.
A verificação de ambas as bibliotecas foi realizada com o uso da ferramenta Hets, que traduz as especificações para a linguagem HOL, gerando necessidades de provas que foram, por sua vez, verificadas com o auxílio do provador de teoremas Isabelle.
Para ilustrar o uso do subconjunto especificado foram incluídas algumas especificações envolvendo listas e tipos booleanos.
Foram encontrados alguns obstáculos no que diz respeito ao uso de subtipos, tais como o uso das especificações numéricas.
Como a solução para este problema fugia ao escopo desse trabalho, a biblioteca não contempla o suporte a tipos de dados numéricos.
Embora tenha-se refinado a biblioteca para suportar tipos com avaliação preguiçosa, não se utilizou os tipos de dados contínuos de HasCASL, fato que impossibilitou a especificação de estruturas infinitas e o refinamento de especificações para o subconjunto executável desta linguagem.
Alguns teoremas permaneceram sem provas devido a dificuldades em utilizar o provador de teoremas Isabelle.
Algumas sugestões de extensão à biblioteca são propostas, tratando, basicamente, do suporte à estruturas infinitas e ao suporte para tipos numéricos.
Concurso Público para Professor Doutor - MS-3
