Aula 7

Instrução de iteração while

2003/2004Introdução à Programação2

passo

[G]

[¬G]

Início da actividade

Fim da actividade

Actividade

Transição

Entroncamento

Ramificação

Instrução while

while(G) passo

GuardaGuarda

2003/2004Introdução à Programação3

potênciaDe()

double potênciaDe(double const x, int const n){ int i = 1; double potência = x;

while(i <= n) { potência *= x; ++i; }

return potência;}

2003/2004Introdução à Programação4

potênciaDe(2.0, 3)

x n i potência i <= n

2.0 3 1 2.0

while(i <= n) { potência *= x; ++i;}

2003/2004Introdução à Programação5

potênciaDe(2.0, 3)

x n i potência i <= n

2.0 3 1 2.0 V

2.0 3

while(i <= n) { potência *= x; ++i;}

2003/2004Introdução à Programação6

potênciaDe(2.0, 3)

x n i potência i <= n

2.0 3 1 2.0 V

2.0 3 4.0

while(i <= n) { potência *= x; ++i;}

2003/2004Introdução à Programação7

potênciaDe(2.0, 3)

x n i potência i <= n

2.0 3 1 2.0 V

2.0 3 2 4.0

while(i <= n) { potência *= x; ++i;}

2003/2004Introdução à Programação8

potênciaDe(2.0, 3)

x n i potência i <= n

2.0 3 1 2.0 V

2.0 3 2 4.0 V

2.0 3

while(i <= n) { potência *= x; ++i;}

2003/2004Introdução à Programação9

potênciaDe(2.0, 3)

x n i potência i <= n

2.0 3 1 2.0 V

2.0 3 2 4.0 V

2.0 3 8.0

while(i <= n) { potência *= x; ++i;}

2003/2004Introdução à Programação10

potênciaDe(2.0, 3)

x n i potência i <= n

2.0 3 1 2.0 V

2.0 3 2 4.0 V

2.0 3 3 8.0

while(i <= n) { potência *= x; ++i;}

2003/2004Introdução à Programação11

potênciaDe(2.0, 3)

x n i potência i <= n

2.0 3 1 2.0 V

2.0 3 2 4.0 V

2.0 3 3 8.0 V

2.0 3

while(i <= n) { potência *= x; ++i;}

2003/2004Introdução à Programação12

potênciaDe(2.0, 3)

x n i potência i <= n

2.0 3 1 2.0 V

2.0 3 2 4.0 V

2.0 3 3 8.0 V

2.0 3 16.0

while(i <= n) { potência *= x; ++i;}

2003/2004Introdução à Programação13

potênciaDe(2.0, 3)

x n i potência i <= n

2.0 3 1 2.0 V

2.0 3 2 4.0 V

2.0 3 3 8.0 V

2.0 3 4 16.0

while(i <= n) { potência *= x; ++i;}

2003/2004Introdução à Programação14

potênciaDe(2.0, 3)

x n i potência i <= n

2.0 3 1 2.0 V

2.0 3 2 4.0 V

2.0 3 3 8.0 V

2.0 3 4 16.0 F

Errado!

A guarda i ≤ n está errada.

2003/2004Introdução à Programação15

potênciaDe()

double potênciaDe(double const x, int const n){ int i = 1; double potência = x;

while(i < n) { potência *= x; ++i; }

return potência;}

2003/2004Introdução à Programação16

potênciaDe(5.0, 0)

x n i potência i < n

5.0 0 1 5.0

while(i < n) { potência *= x; ++i;}

2003/2004Introdução à Programação17

potênciaDe(5.0, 0)

x n i potência i < n

5.0 0 1 5.0 F

Errado!

A inicialização está errada.

2003/2004Introdução à Programação18

potênciaDe()

double potênciaDe(double const x, int const n){ int i = 0; double potência = 1.0;

while(i < n) { potência *= x; ++i; }

return potência;}

2003/2004Introdução à Programação19

Estrutura de um ciclo

inic (inicialização)

while(G) passo

Normalmente passo é

{ acção

prog (progresso)

} prog

[G]

[¬G]

inic

acção

2003/2004Introdução à Programação20

potênciaDe()

E se alguém invoca potênciaDe(2.0, -1)? potênciaDe() devolve erradamente 1.0

Porquê? Pré-condição; ou Implementação

2003/2004Introdução à Programação21

potênciaDe()

/** Devolve a potência n de x. @pre 0 ≤ n. @post potênciaDe = xn. */double potênciaDe(double const x, int const n){ int i = 0; double potência = 1.0;

while(i < n) { potência *= x; ++i; }

return potência;}

2003/2004Introdução à Programação22

potênciaDe()

/** Devolve a potência n de x. @pre 0 ≤ n. @post potênciaDe = xn. */double potênciaDe(double const x, int const n){ int i = 0; double potência = 1.0;

while(i != n) { potência *= x; ++i; }

return potência;}

2003/2004Introdução à Programação23

potênciaDe()

/** Devolve a potência n de x. @pre 0 ≤ n. @post potênciaDe = xn. */double potênciaDe(double const x, int const n){ assert(0 <= n);

int i = 0; double potência = 1.0;

while(i != n) { potência *= x; ++i; }

return potência;}

2003/2004Introdução à Programação24

A reter...

Programação com cinto, liga e suspensórios

Escrever sempre a especificação da rotina

Demonstrar que os ciclos estão correctos

2003/2004Introdução à Programação25

potênciaDe()

/** ... */double potênciaDe(double const x, int const n){ assert(0 <= n);1 int i = 0; double potência = 1.0;2 while(i != n) {3 potência *= x; ++i;4 }5 return potência;}

2003/2004Introdução à Programação26

Asserções nas transições

++i;

[i ≠ n]

[i = n]

int i = 0;double potência = 1.0;

potência *= x;

{PC: 0 ≤ n}

{0 ≤ n i = 0 potência = 1}

{0 ≤ n 0 ≤ i < n potência = xi}

{0 ≤ n 0 < i ≤ n potência = xi}

{0 ≤ n i = n potência = xn}

1

2

3

4

5

2003/2004Introdução à Programação27

Condição Invariante

Condição verdadeira Depois de inicialização Antes do passo Depois do passo Depois do ciclo

Condição correspondente à união dos conjuntos definidos pelas asserções 2, 3, 4 e 5

CI: 0 ≤ i ≤ n potência = xi.

2003/2004Introdução à Programação28

Correcção parcial de um ciclo

1. Descobrir condição invariante (CI)

2. Provar que init estabelece veracidade de CI

3. Provar que CI G seguida de passo CI

4. Provar que CI ¬G CO

2003/2004Introdução à Programação29

init estabelece veracidade de CI

init:

int i = 0; double potência = 1.0;

CI: 0 ≤ i ≤ n potência = xi.

0 ≤ 0 ≤ n 1.0 = x0.

0 ≤ n 1.0 = 1.0.

V V V

Dada a PC, 0 ≤ n, é V.

2003/2004Introdução à Programação30

CI G seguida de passo CI: demonstração directa

while(i != n) { // CI G: 0 ≤ i ≤ n potência = xi i ≠ n // CI G: 0 ≤ i < n potência = xi

potência *= x; // 0 ≤ i < n potência = xi x // 0 ≤ i < n potência = xi + 1

++i; // 0 ≤ (i - 1) < n potência = x(i - 1) + 1

// 1 ≤ i < n + 1 potência = xi

// // CI : 0 ≤ i ≤ n potência = xi

}

2003/2004Introdução à Programação31

CI G seguida de passo CI: demonstração inversa

while(i != n) { // CI G: 0 ≤ i ≤ n potência = xi i ≠ n // CI G: 0 ≤ i < n potência = xi

// 0 ≤ i + 1 ≤ n potência x = xi + 1

// -1 ≤ i ≤ n - 1 potência x = xi + 1

// -1 ≤ i < n potência x = xi + 1

potência *= x; // 0 ≤ i + 1 ≤ n potência = xi + 1

++i; // CI: 0 ≤ i ≤ n potência = xi

}

Implica

2003/2004Introdução à Programação32

CI ¬G CO

CI: 0 ≤ i ≤ n potência = xi.G: i ≠ n.

CI ¬G: 0 ≤ i ≤ n potência = xi i = nCI ¬G: 0 ≤ n ≤ n potência = xn i = nCI ¬G: 0 ≤ n potência = xn i = n

CO: potência = xn

2003/2004Introdução à Programação33

E o ciclo termina sempre?

i começa em 0 (zero) Pré-condição: 0 ≤ n Guarda: i ≠ n Progresso: ++i

Se 0 = n, 0 ≠ 0 é F e o ciclo não é executado Se 0 < n, como i começa em 0 e avança de 1

em 1, n é atingido ao fim de n iterações

2003/2004Introdução à Programação34

A reter...

PC das rotinas tão fraca quanto possível Bom para consumidor Complicado para produtor PC ideal: V

CO das rotinas tão fortes quanto possível Bom para consumidor Complicado para produtor

Guardas dos ciclos tão fracas quanto possível Violação da PC dá origem a ciclo “infinito” que facilita

detecção de erros ao produtor CI dos ciclos tão forte quanto possível

Explica funcionamento do ciclo

2003/2004Introdução à Programação35

Aula 7: Sumário

Instrução while Sintaxe Semântica

Exemplo de ciclos simples Inicialização, guarda, passo (acção e

progresso) Condição invariante Demonstração da correcção de ciclos Importância da fraqueza das guardas