Aula 8
Metodologia de Dijkstra para
desenvolvimento de ciclos
Ciclos



Parte importante da escrita de algoritmos
Impossível demonstrar correcção com testes
Condições invariantes importantes para
demonstrar correcção



2
Verdadeiras do início ao fim dos ciclos
Fortes!
Referem todas instâncias envolvidas
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;
x;
potência *=
++i;
++i;
}
Inicialização
Acção
Passo
Progresso
return potência;
}
3
Introdução à Programação
2003/2004
Diagrama de actividade
inic
{PC: 0 ≤ n}
int i = 0;
double potência = 1.0;
[i = n]
{0 ≤ n  0 ≤ i < n 
potência = xi}
acção
{0 ≤ n  0 < i ≤ n 
potência = xi}
{0 ≤ n  i = 0 
potência = 1}
passo
[i ≠ n]
potência *= x;
{0 ≤ n  i = n 
potência = xn}
++i;
prog
4
Introdução à Programação
2003/2004
Condição invariante
CI: 0 ≤ i ≤ n  potência = xi.

Condição invariante explica funcionamento do
ciclo


5
Durante todo o ciclo potência contém xi,
estando sempre i entre 0 e n
Como i varia entre 0 e n, e termina com n, o
objectivo é atingido
Introdução à Programação
2003/2004
Metodologia de Dijkstra

Edsger Dijkstra



Fundador da programação disciplinada
Programação é uma ciência
Metodologia

Baseia-se na condição objectivo
• Programação é actividade orientada pelos objectivos

6
Condição invariante retirada da condição
objectivo
Introdução à Programação
2003/2004
Soma dos
primeiros n ímpares inteiros
int somaDosPrimeirosÍmpares(int const n)
{
int r = ?;
...
return r;
}
7
Introdução à Programação
2003/2004
Raiz inteira
int raizInteiraDe(int const x)
{
int r = ?;
...
return r;
}
8
Introdução à Programação
2003/2004
1
Especificar o problema
Escrever
o
Pré-condição
o
Condição objectivo
somaDosPrimeirosÍmpares()
/** Devolve a soma dos primeiros n naturais ímpares.
@pre 0 ≤ n.
@post somaDosPrimeirosÍmpares = (S j : 0 ≤ j < n : 2j + 1). */
int somaDosPrimeirosÍmpares(int const n)
{
assert(0 <= n);
// 0 ≤ n.
int r = ?;
...
// CO: r = (S j : 0 ≤ j < n : 2j + 1).
return r;
}
10
Introdução à Programação
2003/2004
raizInteiraDe()
/** Devolve a melhor aproximação por defeito de x1/2.
@pre 0 ≤ x.
@post 0 ≤ raizInteiraDe ≤ x1/2 < raizInteiraDe + 1. */
int raizInteiraDe(int const x)
{
assert(0 <= x);
// 0 ≤ x.
int r = ?;
...
// CO: 0 ≤ r ≤ x1/2 < r + 1.
assert(0 <= r and r * r <= x and x < (r + 1) * (r + 1));
return r;
}
11
Introdução à Programação
2003/2004
2
Será necessário um
ciclo?
Verificar se ciclo é melhor abordagem
o
Análise do problema
o
Intuição!
o
Experiência…
somaDosPrimeirosÍmpares()
/** Devolve a soma dos primeiros n naturais ímpares.
@pre 0 ≤ n.
@post somaDosPrimeirosÍmpares = (S j : 0 ≤ j < n : 2j + 1). */
int somaDosPrimeirosÍmpares(int const n)
{
assert(0 <= n);
// 0 ≤ n.
int r = ?;
while(...) {
...
}
// CO: r = (S j : 0 ≤ j < n : 2j + 1).
return r;
}
13
Introdução à Programação
2003/2004
raizInteiraDe()
/** Devolve a melhor aproximação por defeito de x1/2.
@pre 0 ≤ x.
@post 0 ≤ raizInteiraDe ≤ x1/2 < raizInteiraDe + 1. */
int raizInteiraDe(int const x)
{
assert(0 <= x);
// 0 ≤ x.
int r = ?;
while(...) {
...
}
// CO: 0 ≤ r ≤ x1/2 < r + 1.
assert(0 <= r and r * r <= x and x < (r + 1) * (r + 1));
return r;
}
14
Introdução à Programação
2003/2004
3
Obtenção da condição
invariante
Programar é actividade orientada pelos
objectivos
o
Enfraquecer a CO para obter a CI
somaDosPrimeirosÍmpares()

Substituição de constante na CO por variável
inic
int i = ?;
int r = ?;
Não é equivalente
a CO.
CO: r = (S j : 0 ≤ j < n : 2j + 1).
r = (S j : 0 ≤ j < i : 2j + 1).
CO’: r = (S j : 0 ≤ j < i : 2j + 1)  i = n.
16
Introdução à Programação
2003/2004
somaDosPrimeirosÍmpares()
/** Devolve a soma dos primeiros n naturais ímpares.
@pre 0 ≤ n.
@post somaDosPrimeirosÍmpares = (S j : 0 ≤ j < n : 2j + 1). */
int somaDosPrimeirosÍmpares(int const n)
{
assert(0 <= n);
// 0 ≤ n.
int i = ?;
int r = ?;
while(...) {
...
}
// CO’: r = (S j : 0 ≤ j < i : 2j + 1)  i = n.
// que implica CO: r = (S j : 0 ≤ j < n : 2j + 1).
return r;
}
17
Introdução à Programação
2003/2004
somaDosPrimeirosÍmpares()
CO’: r = (S j : 0 ≤ j < i : 2j + 1)  i = n.

Enfraquecendo as restrições relativas a i
CI: r = (S j : 0 ≤ j < i : 2j + 1)  ? ≤ i ≤ ?.
CI: r = (S j : 0 ≤ j < i : 2j + 1)  0 ≤ i ≤ n.
18
Introdução à Programação
2003/2004
somaDosPrimeirosÍmpares()
/** Devolve a soma dos primeiros n naturais ímpares.
@pre 0 ≤ n.
@post somaDosPrimeirosÍmpares = (S j : 0 ≤ j < n : 2j + 1). */
int somaDosPrimeirosÍmpares(int const n)
{
assert(0 <= n);
// 0 ≤ n.
int i = ?;
int r = ?;
// CI: r = (S j : 0 ≤ j < i : 2j + 1)  0 ≤ i ≤ n.
while(...) {
...
}
// CO’: r = (S j : 0 ≤ j < i : 2j + 1)  i = n.
// que implica CO: r = (S j : 0 ≤ j < n : 2j + 1).
return r;
}
19
Introdução à Programação
2003/2004
raizInteiraDe()
ABCD

Factorização da condição objectivo


Parte é negação da guarda
Parte restante é condição invariante
A
CO: A  B  C  D
CI: A  C

B
AC
D
C
Sabendo que no final do ciclo se quer CI  ¬G  CO
¬G: B  D

20
Logo, CI  ¬G = CO
Introdução à Programação
2003/2004
raizInteiraDe()
CO: 0 ≤ r ≤ x1/2 < r + 1, ou seja
0 ≤ r  r2 ≤ x  x < (r + 1)2 .

Começando a procurar em 0 (zero) e
terminando quando se sabe que o valor
seguinte já não serve…
CI: 0 ≤ r  r2 ≤ x.
¬G: x < (r + 1)2.
21
Introdução à Programação
2003/2004
raizInteiraDe()
/** Devolve a melhor aproximação por defeito de x1/2.
@pre 0 ≤ x.
@post 0 ≤ raizInteiraDe ≤ x1/2 < raizInteiraDe + 1. */
int raizInteiraDe(int const x)
{
assert(0 <= x);
// 0 ≤ x.
int r = ?;
// CI: 0 ≤ r  r2 ≤ x.
while(...) {
...
}
// CO: 0 ≤ r ≤ x1/2 < r + 1.
assert(0 <= r and r * r <= x and x < (r + 1) * (r + 1));
return r;
}
22
Introdução à Programação
2003/2004
4
Determinação da
guarda
Procurar guarda que leve ao resultado
o
CI  ¬G  CO
somaDosPrimeirosÍmpares()
CI  ¬G: r = (S j : 0 ≤ j < i : 2j + 1)  0 ≤ i ≤ n  ¬G.
CO’: r = (S j : 0 ≤ j < i : 2j + 1)  i = n.

Qual a guarda mais simples que garante a verificação da CO?
¬G: i = n.
ou seja,
G: i ≠ n.
CI  ¬G: r = (S j : 0 ≤ j < i : 2j + 1)  0 ≤ i ≤ n  i = n.
CI  ¬G: r = (S j : 0 ≤ j < i : 2j + 1)  0 ≤ n  i = n.
que implica CO.
24
Introdução à Programação
2003/2004
somaDosPrimeirosÍmpares()
/** Devolve a soma dos primeiros n naturais ímpares.
@pre 0 ≤ n.
@post somaDosPrimeirosÍmpares = (S j : 0 ≤ j < n : 2j + 1). */
int somaDosPrimeirosÍmpares(int const n)
{
assert(0 <= n);
// 0 ≤ n.
int i = ?;
int r = ?;
// CI: r = (S j : 0 ≤ j < i : 2j + 1)  0 ≤ i ≤ n.
while(i != n) {
...
}
// CO’: r = (S j : 0 ≤ j < i : 2j + 1)  i = n.
// que implica CO: r = (S j : 0 ≤ j < n : 2j + 1).
return r;
}
25
Introdução à Programação
2003/2004
raizInteiraDe()
CO: 0 ≤ r  r2 ≤ x  x < (r + 1)2 .
CI: 0 ≤ r  r2 ≤ x.

Logo, sabendo que CI  ¬G = CO
¬G: x < (r + 1)2
ou seja,
G: (r + 1)2 ≤ x.
26
Introdução à Programação
2003/2004
raizInteiraDe()
/** Devolve a melhor aproximação por defeito de x1/2.
@pre 0 ≤ x.
@post 0 ≤ raizInteiraDe ≤ x1/2 < raizInteiraDe + 1. */
int raizInteiraDe(int const x)
{
assert(0 <= x);
// 0 ≤ x.
int r = ?;
// CI: 0 ≤ r  r2 ≤ x.
while((r + 1) * (r + 1) <= x) {
...
}
// CO: 0 ≤ r ≤ x1/2 < r + 1.
assert(0 <= r and r * r <= x and x < (r + 1) * (r + 1));
return r;
}
27
Introdução à Programação
2003/2004
5
Determinação da
inicialização
Escolher inicialização tão simples quanto
possível:
o
Sabendo que PC é verdadeira
o
Garantir verificação da CI
somaDosPrimeirosÍmpares()
/** Devolve a soma dos primeiros n naturais ímpares.
@pre 0 ≤ n.
@post somaDosPrimeirosÍmpares = (S j : 0 ≤ j < n : 2j + 1). */
int somaDosPrimeirosÍmpares(int const n)
{
assert(0 <= n);
// 0 ≤ n.
int i = ?;
int r = ?;
// CI: r = (S j : 0 ≤ j < i : 2j + 1)  0 ≤ i ≤ n.
while(i != n) {
...
}
// CO’: r = (S j : 0 ≤ j < i : 2j + 1)  i = n.
// que implica CO: r = (S j : 0 ≤ j < n : 2j + 1).
return r;
}
29
Introdução à Programação
2003/2004
somaDosPrimeirosÍmpares()
/** Devolve a soma dos primeiros n naturais ímpares.
@pre 0 ≤ n.
@post somaDosPrimeirosÍmpares = (S j : 0 ≤ j < n : 2j + 1). */
int somaDosPrimeirosÍmpares(int const n)
{
assert(0 <= n);
// 0 ≤ n.
int i = 0;
int r = 0;
// CI: r = (S j : 0 ≤ j < i : 2j + 1)  0 ≤ i ≤ n.
while(i != n) {
...
}
// CO’: r = (S j : 0 ≤ j < i : 2j + 1)  i = n.
// que implica CO: r = (S j : 0 ≤ j < n : 2j + 1).
return r;
}
30
Introdução à Programação
2003/2004
raizInteiraDe()
/** Devolve a melhor aproximação por defeito de x1/2.
@pre 0 ≤ x.
@post 0 ≤ raizInteiraDe ≤ x1/2 < raizInteiraDe + 1. */
int raizInteiraDe(int const x)
{
assert(0 <= x);
// 0 ≤ x.
int r = ?;
// CI: 0 ≤ r  r2 ≤ x.
while((r + 1)*(r + 1) <= x) {
...
}
// CO: 0 ≤ r ≤ x1/2 < r + 1.
assert(0 <= r and r * r <= x and x < (r + 1) * (r + 1));
return r;
}
31
Introdução à Programação
2003/2004
raizInteiraDe()
/** Devolve a melhor aproximação por defeito de x1/2.
@pre 0 ≤ x.
@post 0 ≤ raizInteiraDe ≤ x1/2 < raizInteiraDe + 1. */
int raizInteiraDe(int const x)
{
assert(0 <= x);
// 0 ≤ x.
int r = 0;
// CI: 0 ≤ r  r2 ≤ x.
while((r + 1)*(r + 1) <= x) {
...
}
// CO: 0 ≤ r ≤ x1/2 < r + 1.
assert(0 <= r and r * r <= x and x < (r + 1) * (r + 1));
return r;
}
32
Introdução à Programação
2003/2004
6
Escolha de um
progresso
Um ciclo tem de terminar
o
Num número finito de passos
o
Rapidamente? Pode valer a pena
investigar progressos complexos
somaDosPrimeirosÍmpares()
/** ... */
int somaDosPrimeirosÍmpares(int const n)
{
assert(0 <= n);
// 0 ≤ n.
int i = 0;
int r = 0;
// CI: r = (S j : 0 ≤ j < i : 2j + 1)  0 ≤ i ≤ n.
while(i != n) {
acção
++i;
}
// CO’: r = (S j : 0 ≤ j < i : 2j + 1)  i = n.
// que implica CO: r = (S j : 0 ≤ j < n : 2j + 1).
return r;
}
34
Introdução à Programação
2003/2004
raizInteiraDe()
/** ... */
int raizInteiraDe(int const x)
{
assert(0 <= x);
// 0 ≤ x.
int r = 0;
// CI: 0 ≤ r  r2 ≤ x.
while((r + 1)*(r + 1) <= x) {
acção
++r;
}
// CO: 0 ≤ r ≤ x1/2 < r + 1.
assert(0 <= r and r * r <= x and x < (r + 1) * (r + 1));
return r;
}
35
Introdução à Programação
2003/2004
7
Determinação da acção
Escolher acção tal que
// CI e G.
acção
prog
// CI.
Garante veracidade de
CI apesar do progresso
somaDosPrimeirosÍmpares()
// CI: r = (S j : 0 ≤ j < i : 2j + 1)  0 ≤ i ≤ n.
while(i != n) {
// CI  G: r = (S j : 0 ≤ j < i : 2j + 1)  0 ≤ i ≤ n  i ≠ n.
// CI  G: r = (S j : 0 ≤ j < i : 2j + 1)  0 ≤ i < n.
acção
// r = (S j : 0 ≤ j < i + 1 : 2j + 1)  0 ≤ i + 1 ≤ n.
// r = (S j : 0 ≤ j < i + 1 : 2j + 1)  -1 ≤ i < n.
++i;
// CI: r = (S j : 0 ≤ j < i : 2j + 1)  0 ≤ i ≤ n.
}
Falta um termo ao somatório.
37
Introdução à Programação
2003/2004
somaDosPrimeirosÍmpares()
/** ... */
int somaDosPrimeirosÍmpares(int const n)
{
assert(0 <= n);
// 0 ≤ n.
int i = 0;
int r = 0;
// CI: r = (S j : 0 ≤ j < i : 2j + 1)  0 ≤ i ≤ n.
while(i != n) {
r += 2 * i + 1;
++i;
}
// CO’: r = (S j : 0 ≤ j < i : 2j + 1)  i = n.
// que implica CO: r = (S j : 0 ≤ j < n : 2j + 1).
return r;
}
38
Introdução à Programação
2003/2004
raizInteiraDe()
// CI: 0 ≤ r  r2 ≤ x.
while((r + 1)*(r + 1) <= x) {
// CI  G: 0 ≤ r  r2 ≤ x  (r + 1) 2 ≤ x.
// CI  G: 0 ≤ r  (r + 1) 2 ≤ x.
acção
// 0 ≤ r + 1  (r + 1) 2 ≤ x.
// -1 ≤ r  (r + 1) 2 ≤ x.
++r;
// CI: 0 ≤ r  r2 ≤ x.
Não é necessária
}
acção!
39
Introdução à Programação
2003/2004
raizInteiraDe()
/** ... */
int raizInteiraDe(int const x)
{
assert(0 <= x);
// 0 ≤ x.
int r = 0;
// CI: 0 ≤ r  r2 ≤ x.
while((r + 1)*(r + 1) <= x)
++r;
// CO: 0 ≤ r ≤ x1/2 < r + 1.
assert(0 <= r and r * r <= x and x < (r + 1) * (r + 1));
return r;
}
40
Introdução à Programação
2003/2004
8
E se alguma coisa
falhar?
Voltar atrás
 acção ou inic demasiado complexas
 CI menos boa
 ...
Será que na soma dos ímpares o
ciclo é necessário?
Inteiros na base 1
1: *
2: **
3: ***
Impares
1:
3:
5:
4: ****
5: *****
...
42
7:
Soma dos primeiros
4 ímpares
*
1+3+5+7
*
**
*
*
***
=
*
*
*
*
****
Introdução à Programação
2003/2004
Será que na soma dos ímpares o
ciclo é necessário?
Inteiros na base 1
1: *
2: **
3: ***
Impares
1:
3:
5:
4: ****
5: *****
...
43
7:
Soma dos primeiros
4 ímpares
*
1+3+5+7
*
**
=
*
*
***
**
**
*
*
*
****
Introdução à Programação
2003/2004
Será que na soma dos ímpares o
ciclo é necessário?
Inteiros na base 1
1: *
2: **
3: ***
Impares
1:
3:
5:
4: ****
5: *****
...
44
7:
Soma dos primeiros
4 ímpares
*
1+3+5+7
*
**
*
*
***
=
***
***
***
*
*
*
****
Introdução à Programação
2003/2004
Será que na soma dos ímpares o
ciclo é necessário?
Inteiros na base 1
1: *
2: **
3: ***
Impares
1:
3:
5:
4: ****
5: *****
...
45
7:
Soma dos primeiros
4 ímpares
*
1+3+4+7
*
**
*
*
***
*
*
*
****
Introdução à Programação
=
****
****
****
****
2003/2004
somaDosPrimeirosÍmpares()
/** Devolve a soma dos primeiros n naturais ímpares.
@pre 0 ≤ n.
@post somaDosPrimeirosÍmpares = (S j : 0 ≤ j < n : 2j + 1). */
int somaDosPrimeirosÍmpares(int const n)
{
assert(0 <= n);
return n * n;
}
46
Introdução à Programação
2003/2004
Aula 8: Sumário




Importância da especificação do problema
Noção de invariante de um ciclo
Condição invariante, inicialização e guarda de um ciclo
Metodologia de Dijkstra para desenvolvimento de ciclos:






Obtenção da condição invariante
Obtenção da guarda
Inicialização
Progresso
Acção
Importância da metodologia:





Base formal para desenvolvimento
Controlo dos erros
Redução de surpresas
Melhor raciocínio
Maior eficiência

Prática da construção de ciclos: usar ou não usar metodologia?
47
Introdução à Programação
2003/2004