Upload
internet
View
108
Download
2
Embed Size (px)
Citation preview
Aula 8
Metodologia de Dijkstra para desenvolvimento de ciclos
2003/2004Introdução à Programação2
Ciclos
Parte importante da escrita de algoritmos Impossível demonstrar correcção com testes Condições invariantes importantes para
demonstrar correcção Verdadeiras do início ao fim dos ciclos Fortes! Referem todas instâncias envolvidas
2003/2004Introdução à Programação3
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;}
Inicialização
Passopotência *= x;
Acção
++i;
Progresso
2003/2004Introdução à Programação4
Diagrama de actividade
++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}
inic
prog
acção
passo
2003/2004Introdução à Programação5
Condição invariante
CI: 0 ≤ i ≤ n potência = xi.
Condição invariante explica funcionamento do ciclo 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
2003/2004Introdução à Programação6
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
Condição invariante retirada da condição objectivo
2003/2004Introdução à Programação7
Soma dosprimeiros n ímpares inteiros
int somaDosPrimeirosÍmpares(int const n){ int r = ?;
...
return r;}
2003/2004Introdução à Programação8
Raiz inteira
int raizInteiraDe(int const x){ int r = ?;
...
return r;}
1 Especificar o problema
Escrevero Pré-condiçãoo Condição objectivo
2003/2004Introdução à Programação10
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;}
2003/2004Introdução à Programação11
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;}
2 Será necessário um ciclo?
Verificar se ciclo é melhor abordagemo Análise do problemao Intuição!o Experiência…
2003/2004Introdução à Programação13
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;}
2003/2004Introdução à Programação14
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;}
3 Obtenção da condiçãoinvariante
Programar é actividade orientada pelos
objectivoso Enfraquecer a CO para obter a CI
2003/2004Introdução à Programação16
somaDosPrimeirosÍmpares()
Substituição de constante na CO por variável
inic
int i = ?;int r = ?;
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.
Não é equivalente a CO.
2003/2004Introdução à Programação17
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;}
2003/2004Introdução à Programação18
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.
2003/2004Introdução à Programação19
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;}
2003/2004Introdução à Programação20
raizInteiraDe()
Factorização da condição objectivo Parte é negação da guarda Parte restante é condição invariante
CO: A B C D
CI: A C
Sabendo que no final do ciclo se quer CI ¬G CO
¬G: B D
Logo, CI ¬G = CO
A
B
C
D
A B C D
A C
2003/2004Introdução à Programação21
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.¬¬GG: : xx < ( < (rr + 1) + 1)22..
2003/2004Introdução à Programação22
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;}
4 Determinação da guarda
Procurar guarda que leve ao resultadoo CI ¬G CO
2003/2004Introdução à Programação24
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.
2003/2004Introdução à Programação25
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;}
2003/2004Introdução à Programação26
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.
2003/2004Introdução à Programação27
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;}
5 Determinação da inicialização
Escolher inicialização tão simples quanto
possível:o Sabendo que PC é verdadeirao Garantir verificação da CI
2003/2004Introdução à Programação29
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;}
2003/2004Introdução à Programação30
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;}
2003/2004Introdução à Programação31
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;}
2003/2004Introdução à Programação32
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;}
6 Escolha de um progresso
Um ciclo tem de terminaro Num número finito de passoso Rapidamente? Pode valer a pena
investigar progressos complexos
2003/2004Introdução à Programação34
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;}
2003/2004Introdução à Programação35
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;}
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
2003/2004Introdução à Programação37
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.
2003/2004Introdução à Programação38
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;}
2003/2004Introdução à Programação39
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!
2003/2004Introdução à Programação40
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;}
8 E se alguma coisa falhar?
Voltar atrás acção ou inic demasiado complexas CI menos boa ...
2003/2004Introdução à Programação42
Será que na soma dos ímpares o ciclo é necessário?Inteiros na base 1
1: *
2: **
3: ***
4: ****
5: *****
...
Impares
1: *
3: * **
5: * * ***
7: * * * ****
Soma dos primeiros4 ímpares
1 + 3 + 5 + 7
=
*
2003/2004Introdução à Programação43
Será que na soma dos ímpares o ciclo é necessário?Inteiros na base 1
1: *
2: **
3: ***
4: ****
5: *****
...
Impares
1: *
3: * **
5: * * ***
7: * * * ****
Soma dos primeiros4 ímpares
1 + 3 + 5 + 7
=
** **
2003/2004Introdução à Programação44
Será que na soma dos ímpares o ciclo é necessário?Inteiros na base 1
1: *
2: **
3: ***
4: ****
5: *****
...
Impares
1: *
3: * **
5: * * ***
7: * * * ****
Soma dos primeiros4 ímpares
1 + 3 + 5 + 7
=
*** *** ***
2003/2004Introdução à Programação45
Será que na soma dos ímpares o ciclo é necessário?Inteiros na base 1
1: *
2: **
3: ***
4: ****
5: *****
...
Impares
1: *
3: * **
5: * * ***
7: * * * ****
Soma dos primeiros4 ímpares
1 + 3 + 4 + 7
=
****************
2003/2004Introdução à Programação46
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;}
2003/2004Introdução à Programação47
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?