Estudo de Caso: Raiz Quadrada
Programming from Specifications
Carroll Morgan Prentice-Hall, 1994
[Capítulo 7]
Equipe:
Alysson Barros
Cleber Ribeiro
Capítulo 7 – Estudo de Caso da Raiz Quadrada
Introdução


Aplicação prática e exemplo de aplicação da lei de
refinamentos;
O encontro de invariantes ajuda-nos a refresca os
assunto já visto.
Capítulo 7 – Estudo de Caso da Raiz Quadrada
Programa Abstrato: O ponto de início


Dados um número natural s, atribuímos a um
número natural r, o inteiro mais próximo que não
exceda a raiz quadrada de s (√s).
 Por Exemplo: s = 29, r = 5.
O programa abstrato:
 var r,s : N
 rr :=
: [√s]
s
 
Capítulo 7 – Estudo de Caso da Raiz Quadrada
Programa Abstrato: O ponto de início


No programa abstrato, os símbolos utilizados não
são códigos: √ e   ;
Nosso trabalho seguinte é remover esse símbolos
para que eles possam ser utilizados em códigos
de um linguagem de programação.
Capítulo 7 – Estudo de Caso da Raiz Quadrada
Removendo os operadores ‘exóticos’


Chamamos de exóticos por não serem tratados
como códigos;
O primeiro passo é remover a função de raiz e a
função piso do programa:

Simples especificação 1.7 : r: [ r = [√s]]

Definição de

Definição de √ : r : [ r² ≤ s < (r + 1) ²]
  : r : [ r ≤ √s < r + 1]
Capítulo 7 – Estudo de Caso da Raiz Quadrada
Removendo os operadores ‘exóticos’



Podemos observar que a designação do programa
está escrito agora para o cliente;
Usou-se o poder dos operadores, deixando as
expressões limpas e sucintas;
Nossa tarefa agora é mover de uma designação
para uma especificação:


A especificação é mais fácil para desenvolver;
Necessitamos de uma fórmula no lugar de uma expressão para
explanar as definições das funções raiz e piso.
Capítulo 7 – Estudo de Caso da Raiz Quadrada
Procurando a invariante


A pós condição na iteração 5.5 é da forma: inv ^
¬GG.
Investigar a re-escrita para as pós-condições:




r² ≤ s ^ ¬ (s ≥ (r + 1) ²) e
s < (r + 1) ² ^ ¬ (r² > s)
A primeira opção nos deixa com a opção:
do s ≥ (r + 1) ² -> …. od, com a invariante r² ≤ s
A segunda : do r² > s -> ... . od, com invariante s < (r + 1) ²
Capítulo 7 – Estudo de Caso da Raiz Quadrada
Procurando a invariante




r 1  q
2
2
var q : N  q, r : [r  s  q  r  1  q]
I ˆ r 2  s  q 2  q, r : [ I  r  1  q]
q, r : [ I ]
q, r : [ I , I  r  1  q]
Lei 3.3 – Comp. Seq.
Lei 5.5 - Iteração
do r  1  q 
q, r : [r  1  q, I , q  r  q0  r0 ]
od

var p : N  p : [r  1  q, r  p  q];
q, r : [r  p  q, I , q  r  q0  r0 ]
(1)
Capítulo 7 – Estudo de Caso da Raiz Quadrada
Procurando a invariante

2
2
if s  p  q : [s  p  p  q, I , q  q0 ]
s  p 2  r : [s  p 2  r  p, I , r0  r ]
fi
(1)
(2)
(3)
 q, r : s  1,0
 p : (q  r )  2
 q : p
 r : p
(2) Lei 4.1
(3) Lei 4.1
Capítulo 7 – Estudo de Caso da Raiz Quadrada
Código Final
var q : N  q, r : s  1,0;
do r  1  q 
p : (q  r )  2
if
s  p 2  q : p
s  p 2  r : p
fi
od
r
valor
p1
p3
p2
q