Utilização das regras B-INV e G-INV no STeP

Nesta secção é apresentada uma sessão guiada de utilização do STeP onde se pretende exemplificar a aplicação dos conceitos anteriores. O primeiro passo consiste em escrever o programa em SPL da figura 4.2 num ficheiro de texto. Depois é necessário escrever um ficheiro de especificação com as duas propriedades que pretendemos provar. Este ficheiro deverá conter algo como:

SPEC

PROPERTY no fim x tem o valor 2 : l1 ==> x=2
PROPERTY x e sempre positivo : [] x>=0

Após ligar o STeP começa-se por carregar o programa e depois o ficheiro de especificação (opções Load program e Load specification do menu File). Após estas operações aparece como objectivo de prova a primeira propriedade do ficheiro de especificação. Como pretendemos provar primeiro $\Box x \geq 0$ é necessário trocar o objectivo de prova. Para tal utiliza-se a opção Select search do menu Properties, seleccionando-se a propriedade x e sempre positivo na janela mostrada.

Para provar a validade de $\Box x \geq 0$ vamos utilizar, tal como já foi descrito anteriormente, a regra B-INV pois x>=0 é um invariante indutivo do programa em questão. Para aplicar esta regra selecciona-se o botão B-INV no lado direito da janela do STeP. Após esta operação pode ler-se no rodapé da janela que a aplicação desta regra gerou três novos objectivos de prova. Como este programa só tem uma transição era de esperar que apenas fossem gerados dois objectivos correspondentes às duas premissas da regra B-INV. Esta situação explica-se pelo facto de o STeP implementar a regra B-INV à custa da regra G-INV usando como fórmula mais "forte" a própria propriedade que se pretende provar. Assim, a aplicação da regra B-INV gera três objectivos de prova, sendo o primeiro aquele que corresponde à primeira premissa de G-INV, que nestas situações é sempre trivialmente verdadeiro, razão pela qual a fórmula que é mostrada resume-se simplesmente a true. Para concluir a prova desta fórmula é suficiente precionar o botão Simplify, sendo mostrada uma mensagem que indica que a fórmula foi simplificada para verdadeiro que indica sempre o fim da prova de uma fórmula.

O segundo objectivo de prova corresponde à prova de inicialidade, ou seja, à primeira premissa da regra B-INV. Em vez da fórmula

$\begin{displaymath}x=0 \land l0 \land \lnot l1 \supset x \geq 0 \end{displaymath}$

$\begin{displaymath}x=0 \land l0 \supset x \geq 0 \end{displaymath}$

$\begin{displaymath}x=0 \land pi0=0 \supset x \geq 0 \end{displaymath}$

Finalmente, resta provar que a única transição do programa preserva a propriedade $x \geq 0$ . Na metade superior da janela é apresentado este objectivo numa notação semelhante à da segunda premissa de B-INV, i.é, $\{p\} \tau \{p\}$ , onde a transição $\tau$ é apresentada na notação típica do STeP. Invocando a opção Simplify verifica-se que, neste caso, o STeP não consegue concluir a prova embora a fórmula $x \geq 0 \land l0 \supset x+2 \geq 0$ resultante seja obviamente verdadeira. Esta situação deve-se ao facto de o método de simplificação usado por omissão no STeP não incluir toda a axiomatização da aritmética, que é necessária para provar esta fórmula. O "poder" do mecanismo de simplificação pode ser controlado através da opção Simplification Flags do menu Settings. Para provar automaticamente esta fórmula devemos indicar, na janela que é aberta por essa opção, que pretendemos usar advanced decision procedures no mecanismo de simplificação. Esta opção permite incluir, entre outros, todos os axiomas da aritmética. Se, após fecharmos a janela das opções de simplificação, invocarmos a opção Simplify verifica-se que a fórmula já é provada automaticamente. Como já não existem mais objectivos em aberto aparece a mensagem The proof is COMPLETE indicando que a prova da primeira propriedade foi concluída com sucesso.

É importante notar-se que existe um compromisso básico entre velocidade e "poder" na parametrização do mecanismo de simplificação. Quanto mais opções forem seleccionadas na janela Simplification Flags mais lento será o mecanismo de simplificação (podendo mesmo bloquear). Como tal à que ter o cuidado de apenas seleccionar as opções mais avançadas quando não se conseguir concluir a prova de outra forma mais eficiente (com a prática, poderá mesmo ser mais rápido fazer a prova interactivamente do que usar um mecanismo de simplificação muito avançado).

Como se constata na sessão descrita até ao momento, a primeira opção que se invoca em cada premissa resultante de aplicar uma regra é sempre a opção Simplify. Para evitar fazer essa tarefa manualmente podemos indicar, usando a opção Automatic-Simplify/Check-Valid/OFF do menu Settings que pretendemos usar auto-simplificação. Se seleccionarmos uma vez essa opção este mecanismo é activado, sendo esse facto indicado pela mensagem Auto Simplify no topo da janela. Com a auto-simplificação activada vamos tentar aplicar a regra B-INV na prova da propriedade $l1 \Rightarrow x=2$ . Após pressionado o botão B-INV verificamos que os dois primeiros objectivos de prova foram concluidos automaticamente, restando o objectivo respeitante à segunda premissa de B-INV. Note-se que, com a opção Auto Simplify, quando um objectivo não consegue ser provado automaticamente, a fórmula apresentada corresponde à versão não simplificada. Assim, faz sentido voltar a invocar a opção Simplify no objectivo resultante. Tal como esperado a fórmula resultante é $l0 \supset x=0$ que não sendo genericamente válida impede a conclusão da prova usando directamente a regra B-INV.

Para provar $l1 \Rightarrow x=2$ podemos então seguir duas estratégias: usar a regra G-INV ou proceder a uma prova incremental. Para demonstrar a utilização da primeira estratégia é necessário repor o objectivo de prova inicial. Para tal invoca-se a opção Undo duas vezes seguidas para anular os dois passos da prova já efectuados. Depois invocamos a regra G-INV, aparecendo uma janela onde nos é pedido para introduzir a propriedade mais "forte" $\varphi$ . Como já foi visto anteriormente, neste caso iremos optar por

$\begin{displaymath}(l1 \supset x=2) \land (l0 \supset x=0) \end{displaymath}$

Após modificar a fórmula apresentada por omissão para a fórmula anterior (transcrita na notação do STeP) pressionamos o botão OK. Como a opção Auto Simplify ainda está activa, verifica-se que o mecanismo de simplificação consegue concluir automaticamente a prova de todas as premissas, terminando a prova.

Como não há mais nenhum objectivo de prova é necessário voltar a ler o ficheiro de especificação para se poder demonstrar a segunda estratégia para provar $l1 \Rightarrow x=2$ . Neste caso começamos por provar o invariante auxiliar $l0 \Rightarrow x=0$ . Para introduzir este lema utilizamos a opção Enter new goal do menu Properties. Depois de introduzido o invariante auxiliar, a sua prova faz-se automaticamente através da invocação da regra B-INV. Como todos as propriedades já provadas são usadas pelo STeP na prova de novas propriedades, a prova da propriedade $l1 \Rightarrow x=2$ pode agora ser realizada automaticamente através da aplicação da regra B-INV. Desta forma se conclui esta sessão guiada de utilização do STeP.