Usando Grules

O uso de grules aumenta significativamente o grau de automação de uma prova, pois em situações específicias elimina a necessidade do especificador lidar com problemas referentes a tipos e restrições de valores durante a prova de teoremas (Domain Check e Preconditions por exemplo). Abaixo descrevo como inserir uma grule no Sistema Policial e depois apresento um conjunto de exemplos de situações em que grules podem ser utilizadas.

A quarta versão do Sistema Policial não adiciona nenhuma mudança substancial. Apenas foi adicionado na prova uma regra de automação do tipo grule. O teorema

\begin{theorem}{grule gCPFMaxType}
CPF \in \power \num
\end{theorem}

é usado para dizer ao Z/Eves qual tipo maximal de CPF, sem que seja necessário realizar a expansão de CPF. Isto é, se durante a prova de alguma operação o Z/Eves produzir como objetivo de prova o predicado:

CPF \in \power \num

Então este predicado será convertido a true sem que seja necessário invocar a definição de CPF.

O Z/Eves gera grules quando são definidas constantes em axiomatic-box e generic-box como pode ser observado no Reference Manual 1.5, pag. 20. Free types e schemas também geram grules (descobri isto mexendo). Para mais informações sobre grule consulte o Z/Eves User's Guide 2.3, pag. 41. Um link para um arquivo contendo um conjunto de exemplos ilustrando o uso de grules no Z/Eves está disponível no final da página. Abaixo, discuto estes exemplos.

Grules_Example01 - São definidos dois tipos. É apresentado um teorema em que o predicado envolve o tipo maximal dos tipos defindos antes. Note que para provar este teorema o especificador precisa instruir o Z/Eves manualmente (realizando expansão - i.e., Invoke).

Grules_Example02 - O mesmo exemplo anterior, só que agora foi criada uma grule para informar ao Z/Eves o tipo maximal de B. Para provar o teorema sobre o tipo de B não é necessário expandir B.

Voce deveria notar nos dois exemplos anteriores que o Z/Eves não criou nenhum teorema para os tipos inseridos pelo usuário. Foram inseridos given sets e abbreviations. Nestas situações o especificador deve se encarregar de criar grules para os tipos, se houver necessidade.

Grules_Example03 - Um exemplo maior, utilizando given sets e schemas. Note que quando um schema é definido e é utilizado como tipo, o Z/Eves gera automaticamente a grule SchemaName$declaration. Note também que, se um schema é definido e não é utilizado como tipo, o Z/Eves não gera a regra de automação do tipo grule para o schema. Neste exemplo, o tipo C não foi utilizado como tipo e por isso o Z/Eves não gerou uma grule associada a TIPO_C.

Grules_Example04 - O exemplo anterior, com uma grule adicionada para TIPO_C. A grule não está provada. Não consegui realizar a prova desta grule. Se conseguir, envie-me a resolução. Thanks ;-)

Grules_Example05 - Neste exemplo uma grule é utilizada para adicionar informação sobre restrição de valor. Para isto, dois valores, minvalue e maxvalue, foram definidos através de um axiomatic-box. Ainda no axiomatic-box há uma rule relacionando os dois valores através do predicado: minvalue \leq maxvalue

No teorema ListInitialisation um dos goals é mostrar que: 0 \leq minvalue. A grule foi utilizada para evitar que o especificador tivesse que lidar com a expansão de \nat ao realizar a prova de ListInitialisation.

Este teorema foi propositalmente posto em dois lugares, antes e depois da grule. Pretendeu-se assim mostrar o ganho de automação com o uso da grule.

Note que este exemplo difere bastante dos anteriores, pois usou grules para adicionar informação sobre uma restrição de valor e não sobre tipos.


A quarta versão do sistema policial está disponível em: http://www.dcc.ufba.br/~diego052/experimento/zevesblog/SistemaPolicial_v4.zip


O arquivo de exemplos de uso de grules está disponível em: http://www.dcc.ufba.br/~diego052/experimento/zevesblog/Grules_Examples_01-05.zip