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

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 2 ≤ n < v 2 , u + 1 ≤ v u + 1 = $0 \leq u^2 \leq n < (u + 1)^2$$0 \leq u^2 \leq n < v^2, u + 1 \leq v$$u + 1 = v$

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 .

$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+1 \neq v$$u = \text{[this interesting thing]}$$v = \text{[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.$u$$v$$u$$v$$n+1$$0 \le u \le v \le n+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 ).$u$$v$$u$$v$$x = u = v$$u$$v$$u < v$$u$$v$$u+1 \le v$

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+1$$u^2 \le n < v^2$$0 \le u^2$$n$$n$$n$

• nós temos ;$u \le x \le v$
• quando , escolhemos o próximo como , de modo que (e não muda);u x u 2 ≤ n $x^2 \le n$$u$$x$$u^2 \le n$$v$
• quando , escolhemos o próximo como , de modo que (e não muda).v x n < v 2$x^2 > n$$v$$x$$n < v^2$$u$

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).$u^2 \le n < v^2$

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 $u^2 \le n$$(u+1)^2 > n$$u$$n$