바이너리 검색을위한 불변량 처리하기

Question

이 코드에 대한 불변식이 무엇인지 알아 내야합니다. 나는 복수의 불변성이있을 수 있다고 생각하지만 주제와 온라인 자원을 이해하지 못한다.

public class BinarySearchSqrt { 

    /** Integer square root 
    * Calculates the integer part of the square root 
    * of n, i.e. integer s such that 
    * s*s <= n and (s+1)*(s+1) > n 
    * requires n >= 0 
    */ 
    private static int iSqrt(int n) { 
     int l = 0; 
     int r = n; 
     int m = ((l + r + 1)/2); 
     /* loop invariant 
     * : 
     * : 
     */ 
     while (Math.abs(l - m) > 0) { 
      m = ((l + r + 1)/2); 
      if ((m + 1) * (m + 1) > n) { 
       r = m - 1; 
      } else if ((m * m) < n) { 
       l = m + 1; 
      } 
     } 
     return m; 
    } 
    public static void main(String[] args) { 
     System.out.println(iSqrt(15)); 
     System.out.println(iSqrt(16)); 
    } 
} 

이 코드는 정수의 제곱근을 찾기 위해 이진 검색을 사용하지만이 사각형 번호가없는 경우는 가장 가까운 광장 숫자의 제곱근을 반환해야합니다 : 내가 이진 검색을 위해 만든 코드는 이는 정수보다 작습니다.

코드는 작동하지만 나는 불변량이 무엇인지 놓고 실제로 올바른 값을 반환하는 방법을 보여줍니다. 모든 단서/설명은 좋을 것입니다. 감사합니다.

Answer 1

OK, 그래서이 답변이 늦게 거의 반년이지만, 여기 간다 :

루프 불변 단순히 이전 (이후) 보유하고 뭔가 루프의 각 반복이다. 그래서 여기, 우리는 코드가 화살표로 표시된 장소에서 때마다 유효 조건을 찾을 필요가 : 당신이 하나가되도록 연구를 업데이트하고, 각 반복에서, 그래서 여기

while (Math.abs(l - m) > 0) { //  <------------- 
    m = ((l + r + 1)/2); 
    if ((m + 1) * (m + 1) > n) { 
    r = m - 1; 
    } else if ((m * m) < n) { 
    l = m + 1; 
    } 
} 

을 새로운 R 거짓말 새 정수가 가장 작은 정수 < = sqrt (n)에 가깝도록 증가시키면서 l을 갱신함으로써 가장 작은 정수인 < = sqrt (n)에 가깝게 설정합니다. 그래서 루프 불변는 단순히 :

리터 < = 바닥 (SQRT (N)) < = R