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.zipO arquivo de exemplos de uso de grules está disponível em:
http://www.dcc.ufba.br/~diego052/experimento/zevesblog/Grules_Examples_01-05.zip
