A regra B-WAIT

A regra mais simples que se pode usar para estabelecer a validade de fórmula à espera de é apresentada na figura 5.1. Esta regra só pode ser aplicada quando p=q

  

Figure 5.1: Versão simples da regra B-WAIT

Como exemplo de aplicação desta regra vamos provar a validade da fórmula

para o programa não determinístico da figura 5.2.

  

Figure 5.2: Exemplo de programa não determinístico

out y:int where y=1

l0: loop forever do [
        y := y+5
        or
        y := y-1
        or
        guard y<0 do y := y-2
]

Para provar a validade desta fórmula devemos provar

que é equivalente a

As premissas que resultam da aplicação da regra B-WAIT são:

Como são todas trivialmente válidas a propriedade é verdadeira.