Verificação de Algoritmos Funcionais em Rocq

O sistema Rocq é baseado num formalismo que é ao mesmo tempo uma lógica muito expressiva e uma linguagem de programação com um sistema de tipos muito rico. É portanto uma boa plataforma para verificação formal de algoritmos funcionais. O Rocq possui mesmo um mecanismo de extração de programas, que permite extrair o programa a partir da prova da sua especificação (filtrando o conteúdo computacional dos objectos de prova).

Tipos de Dados para Programação

Vejamos alguns exemplos de tipos dados úteis para programação já definidos no sistema.

Algumas operações sobre o tipo bool também são fornecidas: andb (com notação infixa &&), orb (com notação infixa **

), **xorb, implb e negb.

A soma construtiva {A}+{B} de duas proposições A e B.

O tipo sumbool pode ser usado para definir uma construção “if-then-else”. O Rocq Prover aceita a sintaxe “if test then… else …“ quando test tem do tipo bool ou {A}+{B}, com proposições A e B. O seu significado é

match test with

| left H => ...
| right H => ... end.

Podemos chamar a {P}+{~P} o tipo dos “predicados decidíveis”:

Aqui está um exemplo de uma função que verifica se um elemento está numa lista.

Podemos definir e usar uma notação mais conveniente para estes predicados decidíveis.

Sessão Laboratorial

Vamo-nos agora focar na correção de programas funcionais, tendo por base alguns exemplos. Carregue o arquivo lesson3.v no Rocq Prover para correr os exemplos que a seguir de apresentam. Analise as respostas obtidas e resolva os exercícios propostos.

Tipos $\Sigma$

O sistema de tipos de Rocq permite combinar um tipo e um predicado sobre esse tipo. O tipo de dados obtido representa o subconjunto do tipo cujos elementos verificam o predicado.

A convenção sintática para (sig A P) é a construção {x:A | P x}. (O predicado P é a função característica deste conjunto). Podemos construir elementos deste conjunto como (exist x p) sempre que tivermos uma testemunha x:A e a sua justificação p:(P x). Um valor do tipo {x:A | P x} deve conter um componente computacional que diz como obter um valor v e um certificado, uma prova de que v satisfaz o predicado P.

Em termos técnicos, diz-se que sig é uma “soma dependente” ou um Σ-type.

Também existe uma variante sig2 com dois predicados:

A notação para (sig2 A P Q) é **{x:A

P x & Q x}**.

Correção de Programas Funcionais

Em Rocq existem duas abordagens para definir funções e fornecer provas de que elas satisfazem uma determinada especificação:

• Definir essas funções com uma especificação fraca (um tipo simples) e depois adicionar lemas complementares que demonstram a sua correção.
  • Por exemplo, definimos uma função f : A → B e provamos uma afirmação da forma (∀x:A, R x (fx)), onde R é uma relação que codifica o comportamento de entrada/saída pretendido da função.
• Fornecemos uma especificação forte da função.
  • O tipo desta função afirma diretamente que a entrada é um valor x do tipo A e que a saída é a combinação de um valor v do tipo B e uma prova de que v satisfaz (R x v).

Vamos começar por ilustrar estas duas abordagens com dois exemplos muito simples: as funções head e last que dão, respectivamente, o primeiro e o últimos elemento de uma lista. Estas duas funções embora muito simples introduzem uma dificuldade adicional: são funções parciais que só se podem aplicar a listas não vazias.

Parcialidade

O Rocq Prover não permite a definição de funções parciais (ou seja, funções que apresentam erros em tempo de execução para determinadas entradas). No entanto, podemos enriquecer o domínio da função com uma pré-condição que garanta que as entradas inválidas sejam excluídas.

Uma função parcial do tipo A → B pode ser descrita com um tipo da forma (∀x:A,(P x) → B), onde P é um predicado que descreve o domínio da função.

A aplicação de uma função deste tipo requer dois argumentos: um termo t do tipo A e uma prova da pré-condição (P t).

Vajamos o que acontece no caso da função head.

Para superar esta dificuldade precisamos de acrescentar a pré-condição de que a lista não é vazia.

Ao escrever este comando uma prova é lançada e temos construir um termo do tipo l<>nil -> A. Podemos continuar a fazer isso por análise de casos sobre a lista l, usando match, mas neste caso o tipo de retorno do “match” passa a ser uma função de uma prova da pré-condição para o tipo do resultado. Uma ramificação inválida do “match” leva a uma contradição lógica (viola a pré-condição).

“refine term“ é uma tática que se pode aplicar a qualquer objectivo de prova. É semelhante à tática “exact term” com uma diferença: o utilizador pode colocar “buracos” no termo (representados por _). Serão gerados tantos sub-objectivos de prova quantos “buracos” no termo.

Especificação (fraca) + Prova de Correção

A especificação da função head pode então ser feita do seguinte modo:

A sua correção é atestada pelo seguinte lema.

Especificação (forte) com tipos $\Sigma$

Usando tipos Σ (specification types), podemos indicar as restrições da especificação no tipo da função, restringindo o tipo do contradomínio aos valores que satisfazem a especificação.

Vejamos o predicado Last definido indutivamente e o teorema que especifica a função que fornece o último elemento de uma lista.

Ao provar este teorema construímos um habitante deste tipo, e então podemos extrair o conteúdo computacional desta prova, e obter uma função que satisfaz a especificação.

Extração de Programas

O sistema de tipos do Rocq é muito mais rico do que o das linguagens de programação convencionais. As suas funções podem conter subtermos correspondentes a provas que, em termos práticos, não têm interesse em relação ao valor final. Os cálculos feitos nas provas correspondem a verificações que devem ser feitas em tempo de compilação, enquanto o cálculo dos dados reais precisa ser feito para cada valor passado às funções em tempo de execução.

O Rocq tem um mecanismo de extração que faz a filtragem do conteúdo computacional dos termos, e os converte para uma linguagem de programação alvo (Ocaml, Haskell, Scheme ou JSON). A distinção entre os sorts Prop e Set é utilizada para distinguir os aspectos lógicos (que devem ser descarregados durante a extração) dos aspectos computacionais (que devem ser mantidos).

O módulo de extração deve ser carregado explicitamente.

É possível traduzir para diferentes linguagens: Ocaml, Haskell, Scheme ou JSON.

Todos os objetos mencionados e todas as suas dependências no toplevel do Rocq são extraídos. Podemos fazer inline desses elementos para tornar o código mais legível.

Também é possível utilizar os tipos e construtores da linguagem de programação alvo. Por exemplo, podemos querer usar as listas nativas do Haskell em vez do Rocq.

Podemos extrair o conteúdo computacional da prova do último teorema.

Também podemos extratir a função e as suas dependências para um ficheiro

Podemos também converter para Haskell a função head que definimos acima.

Recursividade não estrutural

Quando o padrão de recursão de uma função não é estrutural nos argumentos (i.e. a chamada recursiva não é aplicada directamente a sub-termos do argumento), o Rocq regeira a definição e obriga a que sejam dadas garantias de terminação para essa função.

O comando Function permite codificar diretamente funções recursivas gerais. Ele aceita uma função de medida que especifica como o argumento “diminui” entre chamadas recursivas. Esse comando gera obrigações de prova que devem ser verificadas para garantir a terminação. Para o utilizar é preciso carregar o módulo Recdef da biblioteca standard.

Vejamos o exemplo do algoritmo de divisão Eucludiana

Para finalizar, aproveitamos para provar a correção deste algoritmo.

Exercícios: Encontrará exercícios adicionais em Rocq(3).pdf.