Como o loop invariável é obtido nesse algoritmo de localização de raiz quadrada?

10

Originalmente em math.SE, mas sem resposta lá.

Considere o seguinte algoritmo.

u := 0
v := n+1;
while ( (u + 1) is not equal to v) do
   x :=  (u + v) / 2;
   if ( x * x <= n) 
     u := x;
   else
     v := x;
   end_if
end_while 

onde u, v e n são números inteiros e a operação de divisão é divisão inteira.

  • Explique o que é calculado pelo algoritmo.
  • Usando sua resposta à parte I como a pós-condição para o algoritmo, estabeleça um loop invariável e mostre que o algoritmo termina e está correto.

Na classe, a pós-condição foi e o Invariante é . Eu realmente não entendo como a pós-condição e os invariantes foram obtidos. Eu acho que a condição de postagem era ... o que claramente não é o caso. Então, eu estou pensando em como a pós-condição e a invariante foram obtidas. Também estou pensando em como a pré-condição pode ser obtida usando a pós-condição. 0 u 2n < v 2 , u + 1 v u + 1 = v0u2n<(u+1)20u2n<v2,u+1vu+1=v

Ken Li
fonte
Você conhece a lógica Hoare e espera uma resposta para tocá-la?
Raphael

Respostas:

8

Gilles está certo de que a técnica geral é pescar observações interessantes.

Nesse caso, você pode observar que o programa é uma instância de pesquisa binária, porque possui o seguinte formato:

while i + 1 != k
  j := strictly_between(i, k)
  if f(j) <= X then i := j
  if f(j) > X then k := j

Então você acabou de ligar o seu especial f, X... para o invariante geral para busca binária. Dijkstra tem uma boa discussão sobre pesquisa binária .

rgrig
fonte
7

u+1=v é realmente uma pós-condição do loop while (por que você acha que “claramente” não é o caso?). Esse é sempre o caso de um loop while que não contém a break: quando o loop sai, isso pode ocorrer apenas porque a condição do loop (aqui, ) é falsa. Não é a única coisa que será verdadeira quando o loop terminar aqui (esse algoritmo realmente calcula algo interessante, como você viu em sua classe, então e também são pós-condições), mas é o mais óbvio.u+1vu=[this interesting thing]v=[this interesting thing]

Agora, para encontrar outras propriedades interessantes, não há receita geral. De fato, existe algum sentido formal em que não há receita geral para encontrar invariantes de loop. O melhor que você pode fazer é aplicar algumas técnicas que só funcionam em alguns casos ou, geralmente, procurar observações interessantes (que funcionam cada vez melhor à medida que você fica mais experiente).

Se você executar o loop para algumas iterações com algum valor de , verá isso em cada iteração:n

  • quer salta para ;u(u+v)/2
  • ou pula para .v(u+v)/2

Em particular, começa com menos de nunca o ultrapassará. Além disso, começa positivo e aumenta, enquanto começa em e diminui. Portanto, é invariável ao longo deste programa.uvuvn+10uvn+1

Uma coisa que não é tão óbvia é se pode ser igual a . Isso é importante: se e se tornarem iguais, teremos e o loop continuará para sempre. Portanto, você precisa provar que e nunca se tornam iguais para provar que o algoritmo está correto (ou seja, não faz um loop para sempre). Depois que essa necessidade é identificada, é fácil provar (estou deixando isso como um exercício) que é um loop invariável (lembre-se de que e são números inteiros, portanto isso é equivalente a ).uvuvx=u=vuvu<vuvu+1v

Como no final do programa, a pós-condição que você recebeu também pode ser escrita (a parte é trivial). A razão pela qual queremos uma pós-condição como essa, envolvendo , é que queremos vincular o resultado do programa à entrada . Por que essa condição precisa? Estamos procurando por algo o mais preciso possível e observamos onde aparece dentro do loop:v=u+1u2n<v20u2nnn

  • nós temos ;uxv
  • quando , escolhemos o próximo como , de modo que (e não muda);u x u 2n vx2nuxu2nv
  • quando , escolhemos o próximo como , de modo que (e não muda).v x n < v 2 ux2>nvxn<v2u

Essa dicotomia sugere que talvez o tempo todo. Em outras palavras, suspeitamos que seja um loop invariável. Verificar isso é um exercício para o leitor (lembre-se de verificar se a propriedade é verdadeira inicialmente).u2n<v2

E agora que fizemos tudo isso, vemos que e : é a raiz quadrada de arredondada para o número inteiro mais próximo.( u + 1 ) 2 > n u nu2n(u+1)2>nun

Gilles 'SO- parar de ser mau'
fonte
"Então você precisa provar que u e v se tornam iguais para provar que o algoritmo está correto". Acho que esta frase está faltando um "não".
sepp2k
@ KenLi Como esta é sua pergunta no sentido de Stack Exchange, há alguma melhoria específica que você gostaria?
Gilles 'SO- stop being evil'