Aula 7
Instrução de iteração while
Instrução while
Início da
actividade
while(G)
passo
Transição
Entroncamento
Guarda
Ramificação
[¬G]
[G]
Actividade
passo
2
Introdução à Programação
Fim da
actividade
2003/2004
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;
}
3
Introdução à Programação
2003/2004
potênciaDe(2.0, 3)
x
n
i
potência
2.0
3
1
2.0
i <= n
while(i <= n) {
potência *= x;
++i;
}
4
Introdução à Programação
2003/2004
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;
}
5
Introdução à Programação
2003/2004
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;
}
6
Introdução à Programação
2003/2004
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;
}
7
Introdução à Programação
2003/2004
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;
}
8
Introdução à Programação
2003/2004
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;
}
9
Introdução à Programação
2003/2004
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;
}
10
Introdução à Programação
2003/2004
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;
}
11
Introdução à Programação
2003/2004
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;
}
12
Introdução à Programação
2003/2004
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;
}
13
Introdução à Programação
2003/2004
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.
14
Introdução à Programação
2003/2004
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;
}
15
Introdução à Programação
2003/2004
potênciaDe(5.0, 0)
x
n
i
potência
5.0
0
1
5.0
i < n
while(i < n) {
potência *= x;
++i;
}
16
Introdução à Programação
2003/2004
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.
17
Introdução à Programação
2003/2004
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;
}
18
Introdução à Programação
2003/2004
Estrutura de um ciclo
inic (inicialização)
while(G)
passo

inic
Normalmente passo é
[G]
{
acção
prog (progresso)
acção
prog
}
19
[¬G]
Introdução à Programação
2003/2004
potênciaDe()

E se alguém invoca potênciaDe(2.0, -1)?


20
potênciaDe() devolve erradamente 1.0
Porquê?

Pré-condição; ou

Implementação
Introdução à Programação
2003/2004
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;
}
21
Introdução à Programação
2003/2004
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;
}
22
Introdução à Programação
2003/2004
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;
}
23
Introdução à Programação
2003/2004
A reter...

24
Programação com cinto, liga e suspensórios

Escrever sempre a especificação da rotina

Demonstrar que os ciclos estão correctos
Introdução à Programação
2003/2004
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;
}
25
Introdução à Programação
2003/2004
Asserções nas transições
{PC: 0 ≤ n}
1
int i = 0;
double potência = 1.0;
{0 ≤ n  i = 0 
potência = 1}
2
[i = n]
{0 ≤ n  0 ≤ i < n 
potência = xi}
3
[i ≠ n]
potência *= x;
{0 ≤ n  0 < i ≤ n 
potência = xi}
26
5
{0 ≤ n  i = n 
potência = xn}
++i;
4
Introdução à Programação
2003/2004
Condição Invariante

Condição verdadeira






27
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.
Introdução à Programação
2003/2004
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
28
Introdução à Programação
2003/2004
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
29
Dada a PC, 0 ≤ n,
é V.
Introdução à Programação
2003/2004
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
}
30
Introdução à Programação
2003/2004
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
Implica
// 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
}
31
Introdução à Programação
2003/2004
CI  ¬G  CO
CI: 0 ≤ i ≤ n  potência = xi.
G: i ≠ n.
CI  ¬G: 0 ≤ i ≤ n  potência = xi  i = n
CI  ¬G: 0 ≤ n ≤ n  potência = xn  i = n
CI  ¬G: 0 ≤ n  potência = xn  i = n

CO: potência = xn
32
Introdução à Programação
2003/2004
E o ciclo termina sempre?






33
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
Introdução à Programação
2003/2004
A reter...

PC das rotinas tão fraca quanto possível




CO das rotinas tão fortes 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

34
Bom para consumidor
Complicado para produtor
Guardas dos ciclos tão fracas quanto possível


Bom para consumidor
Complicado para produtor
PC ideal: V
Explica funcionamento do ciclo
Introdução à Programação
2003/2004
Aula 7: Sumário

Instrução while







35
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
Introdução à Programação
2003/2004