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