Traduzindo Funções Recursivas de VDM para Isabelle/HOL

Este artigo fala sobre um método de tradução de definições recursivas de um sistema chamado VDM para outro sistema conhecido como Isabelle/HOL. A ideia é criar templates que possam lidar automaticamente com vários tipos de definições em VDM. Este método foca em garantir que as traduções sejam claras e que automatizem o máximo possível do processo de prova.

VDM e Isabelle/HOL têm algumas diferenças, especialmente na forma como lidam com o conceito de terminação em Funções Recursivas. A terminação é importante porque garante que uma função não vai rodar eternamente sem parar. O artigo vai discutir como podemos traduzir definições recursivas levando essas diferenças em consideração.

Usando esse método de tradução, oferecemos uma extensão para ferramentas existentes que ajudam os usuários a converter definições de VDM para Isabelle/HOL. Isabelle permite que os usuários escrevam especificações, provas e documentação tudo em um só lugar. Os detalhes completos das fontes e das provas envolvidas podem ser encontrados em um repositório específico de ferramentas.

As próximas seções vão fornecer informações de fundo sobre VDM e Isabelle, seguidas de discussões sobre a tradução de tipos básicos, recursão e a estratégia geral de tradução.

#Contexto

O tradutor de VDM para Isabelle/HOL cobre uma ampla gama de estruturas encontradas em VDM. Ele pode gerenciar várias expressões, padrões, tipos e especificações em VDM. O objetivo é garantir que a maioria dos padrões em VDM possa ser traduzida de forma eficaz, e quando não puder, haverá uma forma equivalente de representá-los.

Uma área chave de foco nessa tradução é o tratamento de funções definidas recursivamente. Em VDM, os usuários precisam definir uma função de medida para garantir que a recursão vai terminar. Essa função de medida gera obrigações de prova, que são requisitos para confirmar que a recursão funciona como pretendido.

A estratégia de tradução utilizada aqui segue uma abordagem específica chamada terminação de mudança de tamanho (SCT). Essa abordagem verifica se uma função recursiva pode ser provada como terminadora com base nos valores que ela produz. Se cada cálculo leva a um valor menor, pode-se garantir que a recursão vai eventualmente parar.

#Tipos Básicos de VDM em Isabelle

Em Isabelle, números naturais são representados como um tipo de dado com duas partes: o número zero e uma função sucessora que adiciona um. Isabelle também define inteiros e outros tipos numéricos usando esses números naturais. Conversões de tipo estão disponíveis para ajudar os usuários a transitar entre tipos, mas não há regras implícitas que ampliem os tipos automaticamente.

Em VDM, tipos básicos como números naturais e inteiros têm regras específicas de ampliação que devem ser consideradas. Por exemplo, se ambos os tipos são números naturais, o resultado pode ser um inteiro. Nossa estratégia de tradução trata números naturais de VDM especificamente como um sinônimo de tipo em Isabelle, o que ajuda a simplificar o processo e evita a necessidade de coações de tipo complicadas.

No entanto, isso significa que codificar funções recursivas usando números naturais pode ser mais complexo do que se espera, já que a representação em Isabelle é diferente da de VDM.

Mesmo com essas complexidades, a recursão sobre inteiros, conjuntos ou mapas em VDM ainda ocorre porque esses tipos não têm uma definição construtiva direta em Isabelle.

#Recursão em VDM e Isabelle

Toda definição recursiva precisa de uma forma de justificar que vai terminar. Caso contrário, a recursão pode levar a um loop infinito. Em VDM, essa justificativa vem da medida recursiva, que pega os mesmos inputs da definição recursiva e retorna um número natural que deve diminuir com cada chamada recursiva.

Por exemplo, considere uma função recursiva simples que calcula o fatorial de um número natural. A função de medida usa a própria entrada, e a recursão para quando essa entrada chega a zero. Nesse caso, VDM gera três obrigações de prova que devem ser confirmadas em Isabelle.

Isabelle, por outro lado, permite definições recursivas através de recursão primitiva ou definições gerais de funções que produzem obrigações de prova. O desafio está em garantir que os parâmetros correspondam aos padrões definidos e que as chamadas recursivas vão terminar corretamente.

As definições de funções recursivas em Isabelle podem ser expressas usando dois tipos de sintaxe: uma que tenta provar automaticamente a terminação e outra que requer que os usuários forneçam manualmente prova de terminação. A última é frequentemente necessária em casos onde a função recursiva é mais complexa.

A relação de terminação também deve ser bem fundamentada, o que significa que deve ter uma estrutura ordenada para garantir que a recursão vai terminar. Esse requisito adiciona mais uma camada de complexidade ao processo de tradução.

#Estratégia de Tradução de Recursão em VDM

O objetivo da estratégia de tradução é abordar questões relacionadas à recursão sobre tipos básicos, conjuntos, sequências e mapas, incluindo recursão mútua. Começamos marcando todas as funções recursivas em VDM, mesmo aquelas sem uma medida explícita, para facilitar a tradução usando as funções de Isabelle.

Se Isabelle não conseguir provar automaticamente a terminação necessária, o usuário pode fornecer uma Anotação que define uma relação de medida bem fundamentada. Isso ajuda a estabelecer a relação entre as chamadas recursivas e garante que a tradução terá sucesso.

Durante a tradução, a ferramenta verifica a anotação para garantir que está definida corretamente. Esse processo envolve traduzir as anotações em definições de Isabelle para apoiar a prova de terminação.

A estratégia de tradução também requer que as verificações de VDM sejam explicitamente declaradas como predicados. Por exemplo, conjuntos de VDM devem ser finitos, e seus invariantes de tipo devem valer para cada elemento.

#Recursão Sobre Tipos Básicos de VDM

Para tipos básicos como números naturais, a estratégia de tradução primeiro estabelece uma pré-condição que insiste que o parâmetro é um tipo válido. Em seguida, definimos a função recursiva, retornando um valor indefinido se a pré-condição falhar. As provas de compatibilidade e completude dos padrões são então estabelecidas seguindo os métodos padrão de Isabelle.

A bem-fundação da recursão pode muitas vezes ser estabelecida usando a maquinaria existente de Isabelle, tornando o processo mais suave. Também definimos novos lemas para ajudar na descoberta de provas, reduzindo a carga sobre o usuário.

#Recursão Sobre Conjuntos de VDM

O próximo passo na estratégia de tradução envolve lidar com conjuntos de VDM. Um exemplo comum é uma função que soma os elementos de um conjunto. A função verifica se o conjunto está vazio antes de prosseguir com a soma, escolhendo um elemento arbitrário para usar na recursão.

Definimos uma pré-condição para a função que garante que o conjunto contém apenas números válidos e é finito. Assim como nos tipos básicos, estabelecemos a função recursiva em Isabelle, verificando a pré-condição antes de executar a soma.

A relação de medida deve refletir os processos envolvidos, e as ferramentas de Isabelle podem ser usadas para validar a bem-fundação da relação. A prova de terminação também é construída com base nas pré-condições anteriores e nas condições de filtragem.

#Recursão Sobre Mapas de VDM

A recursão sobre mapas é semelhante à recursão sobre conjuntos. Uma função que soma os valores de um mapa usa técnicas semelhantes, verificando se o mapa está vazio e, se não estiver, escolhendo uma chave para somar o valor associado a ela.

Como antes, as pré-condições garantem que tanto o domínio quanto a imagem do mapa satisfaçam propriedades necessárias. O processo de tradução verifica as condições essenciais para bem-fundação e constrói a relação de medida apropriada para apoiar a prova de terminação.

#Recursão Envolvendo Medidas Complexas

Podemos também aplicar a mesma abordagem de tradução para definições recursivas mais complexas. No entanto, essas definições geralmente exigem que os usuários definam anotações mais detalhadas e lemas adicionais para apoiar o processo de prova.

Por exemplo, considere a famosa função de Ackermann, que é conhecida por sua recursão complexa. A função requer que ambos os parâmetros sejam processados de uma certa maneira, o que envolve medidas adicionais que devem ser definidas em VDM. Os usuários devem fornecer anotações para ajudar Isabelle a inferir corretamente as relações entre as chamadas recursivas.

As medidas usadas na versão de VDM diferem daquelas normalmente vistas em Isabelle, portanto, é essencial estabelecer uma conexão clara entre as duas para que a tradução funcione.

#Exemplos Mais Difíceis

Alguns exemplos são mais desafiadores e exigem uma configuração mais elaborada para a prova. Por exemplo, a função de permutação mostra como pode permutar entre parâmetros decrescentes, e a função de Takeuchi demonstra recursão interna.

Esses exemplos complexos frequentemente revelam como os sistemas de prova podem diferir em seus requisitos. Os usuários devem fornecer medidas específicas e frequentemente fazer intervenções manuais para ajudar Isabelle a gerar as provas necessárias.

#Recursão Mútua

Finalmente, a tradução também leva em conta a recursão mútua, onde VDM permite definições que se chamam mutuamente. Podemos usar algoritmos do verificador de tipo de VDM para identificar essas relações e deduzir as medidas necessárias.

Se o gráfico de recursão não puder ser descoberto automaticamente, os usuários devem anotar uma das definições recursivas mutuamente para indicar os nomes de função esperados envolvidos.

Essencialmente, essas interações exigem que todas as funções relacionadas sejam definidas juntas para garantir uma ligação adequada na configuração da prova.

#Conclusão

Este artigo delineou um método para traduzir funções recursivas de VDM para Isabelle/HOL, focando em tipos básicos, conjuntos, mapas e recursão mútua. As estratégias discutidas permitem uma grande variedade de definições recursivas, incluindo exemplos complexos que requerem medidas adicionais e interação do usuário.

À medida que continuamos a refinar essa estratégia de tradução, ela se tornará uma ferramenta valiosa para usuários que precisam converter suas definições de VDM para Isabelle/HOL, garantindo a correção e a terminação de suas funções recursivas. O trabalho futuro envolve implementar ainda mais essas estratégias em ferramentas existentes para melhorar a usabilidade e automação para os usuários.