Provas assistidas no STeP

Como seria de esperar, o STeP nem sempre consegue fazer automaticamente a prova de todas as propriedades que resultam da aplicação das regras B-INV e G-INV. Quando uma situação destas ocorre é necessário utilizar a opção Interactive e conduzir a prova num modo assistido. Este modo assistido utiliza um cálculo de sequentes adaptado à lógica temporal, cujas regras de inferência são apresentadas na página 95 do manual do STeP [3].

  

Figure 4.4: Programa para calcular o factorial

in x : int where x>=0
local y : int where y=0
out z : int where z=1

ciclo:  while (~(x=y)) do
atrib:          (y,z) := (y+1, (y+1)*z);
fim:

Para exemplificar o modo assistido de prova vamos analizar um pequeno exemplo. Considere o programa da figura 4.4 cujo objectivo é determinar o factorial de x. Na figura 4.5 apresenta-se uma especificação para a correção parcial deste programa.

  

Figure 4.5: Especificação da correção parcial do factorial

SPEC

value fact : int --> int

AXIOM fact0 : [] fact(0)=1
AXIOM factn : [] Forall n:int . (n>0 --> fact(n)=n*fact(n-1))

PROPERTY correcao parcial : fim ==> z=fact(x)

Após ler o programa e a especificação para o STeP aplicamos a regra B-INV para tentar provar a referida propriedade. Assumindo que o STeP está configurado para fazer a simplificação automaticamente, ficará por provar a seguinte propriedade:

$$ciclo \land x=y \supset z=fact(x)$$

Para provar esta propriedade inserimos um lema auxiliar (opção Enter new goal do menu Properties) que especifica um dos invariantes do programa, nomeadamente:

$$\Box z=fact(y)$$

Após aplicar a regra B-INV ficamos com a propriedade:

$$atrib \land z=fact(y) \supset z + y \times z = fact(y+1)$$

A prova desta propriedade implica uma instanciação correcta do axioma factn (presente no ficheiro de especificação) que o STeP não é capaz de fazer. Como tal, iremos fazer a prova desta propriedade no modo assistido.

Após pressionar o botão Interactive abre-se a janela do modo de prova assistido com a propriedade anterior. O comando mais importante do modo assistido é o 1-Step-Propositional que permite aplicar uma das regras de inferência da página 95 do manual do STeP [3]. Caso só exista uma regra possível para aplicar a prova avança segundo essa regra. Se existir mais do que uma conectiva proposicional ou temporal o utilizador tem a possibilidade de escolher qual a regra a aplicar (seleccionando a conectiva desejada). Neste caso, apenas a regra $(\Rightarrow \to)$ pode ser aplicada. Assim, após pressionar o botão 1-Step-Propositional o antecedente da implicação passa para o lado esquerdo do sequente. Se se pressionar o botão 1-Step-Propositional mais uma vez é aplicada a regra $(\land \Rightarrow)$. Como não existem mais conectivas não é possível aplicar mais nenhuma regra de inferência e, como tal, a opção 1-Step-Propositional não produz nenhum resultado. Também se poderia chegar a este estado da prova invocando no ínicio uma das seguintes opções:

• Flatten, que procura separar as conjunções no antecendente e as disjunções no consequente.
• All-Propositional, que aplica repetidamente a opção 1-Step-Propositional até que não existam mais fórmulas com conectivas.
• Simplify, que funciona de forma idêntica ao Simplify da janela principal do STeP, e que procura procura simplificar uma fórmula de acordo com as opções seleccionadas na opção Simplification Flags do menu Settings.

Para testar cada uma destas opções utilize a opção Undo para retroceder no estado da prova até à fórmula inicial, aplicando depois cada uma das opções descritas.

Para continuar a prova precisamos do axioma factn do ficheiro de especificação. Para adicionar esse axioma no lado esquerdo do sequente utilizamos a opção Add-Axiom que permite seleccionar qualquer um dos axiomas ou propriedades previamente provadas. Após seleccionar o axioma factn fechamos a janela pressionando o botão Cancel. Para expandir o termo fact(y+1) é necessário instanciar o axioma factn fazendo n=y+1. Para tal utilizamos a opção Instantiate que permite instanciar quantificadores universais no antecedente, ou quantificadores existenciais no consequente, para valores concretos. Se existir mais do que um quantificador no sequente o utilizador deve escolher qual o que deve ser instanciado. Como neste caso apenas existe um quantificador, após seleccionar a opção Instantiate é imediatamente aberta uma janela onde o utilizador deve indicar a expressão em que será instanciada a variável de quantificação. Neste caso a expressão deve ser y+1.

Seleccionando o botão 1-Step-Propositional é aplicada a regra $(\to \Rightarrow)$ que origina dois sequentes. Este facto pode ser comprovando seleccionando a opção View search do menu e verificando que existe uma ramificação na árvore de prova. Note que o objectivo de prova actual é representado por um nodo branco, sendo os restantes objectivos em aberto representados a cinzento. Os nodos intermédios são apresentados a preto. Se se seleccionar um nodo cinzento podemos mudar o objectivo de prova. Antes de fechar a janela seleccione o objectivo 1.1.1.1.

Para proseguir é necessário substituir, de acordo com as hipóteses presentes no antecedente, z por fact(y) e expandir fact(y+1). Para tal devemos usar a opção Replace que permite substituir termos por termos equivalentes. Após pressionar o botão Replace é necessário dizer qual o termo pelo qual vamos substituir alguma coisa. Podemos começar, por exemplo, pelo termo fact(y). Depois, devemos voltar a seleccionar a opção Replace e seleccionar o termo (y+1)*fact(y+1-1). Para provar o objectivo resultante é suficiente pressionar o botão Simplify.

Passando agora ao objectivo 1.1.1.2, podemos começar por invocar a opção Simplify. Para provar o objectivo resultante é necessário provar que $y \geq 0$. Olhando para o programa verifica-se que essa propriedade é claramente um dos seus invariantes. Como tal, para concluir a prova basta provar que $\Box y \geq 0$ é uma fórmula válida. Como precisamos da regra B-INV para provar essa fórmula devemos abandonar o modo assistido seleccionando a opção Quit do menu. Na janela que aparece basta pressionar o botão OK pois já estão seleccionadas as opções que nos interessam. Depois de regressar à janela principal do STeP introduzimos $\Box y \geq 0$ como um novo objectivo de prova. A sua prova é automática, seleccionando a regra B-INV, desde que previamente seja activada a opção Use advanced decision procedures na janela Simplification flags. Depois de provado o invariante $\Box y \geq 0$ os objectivos em aberto são automaticamente verificados invocando a opção Simplify.