Iteração – Capítulo 5

Programming from Specifications Carroll Morgan Prentice-Hall, 1994

Integrantes:Alex MottaCarlos NascimentoPaulo Maia

Descrição Operacional Iteração = repetição;

Um comando é executado enquanto uma certa condição é válida;

Estrutura:do G0 → prog0

║ G1 → prog1

...

║ Gn → progn

od.

Descrição Operacional “Loops” infinitos

Ex : do true → skip od

“Loop” infinito = abort

Uma iteração finaliza quando todas as suas guardas forem falsas Pode não ocorrer em certos estados

iniciais

Descrição Operacional Ex :

Do 2 | n → n := n ÷ 2 od

Iterações podem ser desmembradas sem afetar seu significado:do G0 → prog =

if G0 then

prog;

do G0 → prog od

fi

Descrição Operacional

= if G0 then

prog;

if G0 then

prog;

do G0 → prog od

fi

fi

Definição de Invariante

Abstrair o número de repetições

Fórmula que, se inicialmente for verdadeira, também será verdadeira a cada iteração, inclusive no final

A iteração mantém a invariante e estabelece adicionalmente a negação das guardas

Invariante - Exemplo

do 2 | n -> n := n ÷ 2 od

Qual a invariante?

pt n = (∃k : N n = 2 ^ k)

Invariante - Alguns Raciocínios

Formalmente: inv é um invariante de do G prog od se w: [inv G , inv] prog

Assumindo-se terminação:w: [inv , inv G] do G prog od

Lei de Refinamento: Informalmente

Exemplo:

n :[pt n , pt n 2 | n)]

do 2 | n n := n od

Lei de Refinamento: Informalmente Terminação tem que ser considerada

Por causa dissow :[ true ^ true, true] skip

concluímos que

w :[ true, true ^ false] do true -> skip od

>>>>>> absurdo!

Terminação de Iterações: Variantes Variante:

Exemplo: do 2 | n n := n od termina porque

Cada repetição decrementa n e n não pode se tornar negativo >>>>> n é o variante da iteração

Expressão inteira que é decrementada por cada repetição, mas nunca abaixo de um limite inferior fixo (geralmente 0).

Especificando o Decréscimo do Variante Um comando que decrementa uma variável

inteiran := n - 1

Especificação n :[n = n - 1] X n :[n < n] X

n :[n = N , n < N]

Especificando o Decréscimo do Variante Variáveis com subscrito 0 (variáveis iniciais)

n :[ n < n0] Novas leis de refinamentoLei 5.1 Fortalecimento da pós-condição

Se pre[w\w0]pos’ pos, entãow :[ pre , pos] w :[ pre , pos’]

Lei 5.2 Atribuição

Se (w = w0)x = x0pre pos[w\E], então w,x:[ pre , pos] w := E

Especificando o Decréscimo do Variante

Lei 5.3 Comando skipSe (w = w0 ) pre pos, então

w :[ pre , pos] skip

As leis anteriores ainda valem

Variáveis Iniciais e o Quadro Se uma variável x não está no quadro, então ela

pode ser referenciada na pós condição tanto como x quanto como xo

Lei 5.4 Contração do quadrow,x :[ pre , pos] w :[ pre , pos[x0\ x] ]

Refinamento da Regra para Iteração

Lei 5.5 - Iteração: seja inv, o invariante, qualquer fórmula;

seja V, o variante, qualquer expressão inteira. Então se GG é a disjunção das guardas,

w: [inv, inv Λ ¬ GG] do ( � i . Giw: [inv, inv Λ Gi, inv Λ

(0 ≤ V < V0)]) od. inv e Gi → não possuem variáveis iniciais. V = V[w\w0].

Refinamento da Regra para Iteração Lei 5.5 – Iteração (abreviada):

w: [inv, inv Λ ¬ GG]

do (� i . Giw: [Gi, inv Λ (0 ≤ V < V0)]) od.

Lei 5.6 – Especificação do variante: seja inv, o invariante, qualquer fórmula;

seja V, o variante, qualquer expressão inteira. Então se GG é a disjunção das guardas,

w: [pre, inv, post] w: [pre Λ inv, inv Λ post].

Lista de Verificação da Iteração

Características das iterações: A invariante é verdade inicialmente

O invariante e a negação da guarda são suficientes.

O corpo da iteração mantém a invariante, contanto que a guarda seja verdadeira

O variante é decrementado pela execução do corpo da iteração, contanto que a guarda e a invariante sejam verdadeiras

O variante não pode ficar menor que zero pelo corpo da iteração, contanto que a guarda e a invariante sejam verdadeiras

Exercício de Fixação Desenvolver o seguinte programa usando

cálculo de refinamento:

do 2 | n n := n od

Invariante: pt n , onde pt n = (∃k : N n = 2 ^ k)

Variante: n

Exercício de Fixaçãon : [ pt n , n = 1 ] Lei 1.1 (Lei do Fortalecimento da pós)n : [ pt n , pt n ^ ¬ (2 | n )]Obrigação de Prova: pt n ^ ¬ (2 | n )] n = 1 Lei 5.5 (Lei da Iteração)

do 2 | n n : [ 2|n ^ pt n , pt n ^ 0 ≤ n < n0 ]

od

Exercício de Fixação Lei 5.6 (Lei da especificação da invariante)do 2 | n

n : [ 2|n , pt n , 0 ≤ n < n0 ]

od Lei 5.2 (Lei da atribuição com variável inicial)

n := n 2Obrigação de Prova: ( n = n0 ) ^ (2 | n ) ^ pt n

pt (n 2 ^ (0 ≤ n < n ) [ n\ n 2]