티스토리 뷰

출처 : https://www.acmicpc.net/problem/2003


Two Pointer Algorithm의 전형적 케이스 중 하나.


사실 그렇게 어려운 것은 아니지만 이게 왜 되는지 100% 이해가 가지 않는 상황에서 증명을 안하고 넘어갈 수는 없었다.


How do we know this algorithm takes care of all possible subsequences when it terminates?


Again, I used Jeff Edmonds Loop Invariants Technique of Proving to demonstrate the algorithm's correctness.


백준 소스보다 좀 더 concise한 코드도 작성 할 수 있었다.



우선 문제의 Specification 을 소개하겠다.




다음은 my pseudocode (following Jeff Edmonds style)




Inner Loop Proof of Correctness





Big Loop Proof of Correctness (Initialization)



Big Loop Proof of Correctness (Maintenance and Termination)



Here is the code




import java.util.*;

/**
 * @author Jeong Tae Bang
 * Feb 4, 2018 for BOJ https://www.acmicpc.net/problem/2003 
 */

public class Main {
    
    public static void main(String args[]) {
        Scanner sc = new Scanner(System.in);
        int n = sc.nextInt();
        int s = sc.nextInt();
        int[] a = new int[n+2]; // only use [1..n], [0 and n+1] are 0
        for (int i = 1; i <= n; i++) {
            a[i] = sc.nextInt();
        }
        
        // inint
        int left = 1;
        int right = 1;
        int sum = a[1];
        int ans = 0;
        
        while (right <= n) {
            while (sum > s) {
                sum -= a[left];
                left += 1;
            }
            if (sum == s) ans += 1;
            right +=1;
            sum += a[right];
        }
        System.out.println(ans);
    }
}


댓글
  • 프로필사진 도쿄와라시바것 ㅅㅂ 뭔소린지.. 하지만 멋있네요~ 2018.02.04 12:03 신고
  • 프로필사진 jeongtaebang Inner-Loop Proof of Correctness Maintenance Error: in <LI'> (since left = i'-1... not i-1)

    For Big Loop Maintenance proof Case 3, for clarification, LI_new refers to the new version of the original LI at the top of the loop redefined with the new value of i; it is not referring to <LI'> of the next iteration of the loop
    2018.06.20 01:29 신고
댓글쓰기 폼