Problem 1. Consider the following program to find the maximum value in an array. Write a Hoare logic proof (decorated program) to prove the given Hoare triple.
{0 < N} int m = A[0]; int i = 1; while (i < N) { if (A[i] > m) m = A[i];
else skip;
i = i + 1;
}
{m = max(A[0],A[1],...,A[N − 1])}
1
2
3
4
5
6
7
8
9
10
11
Problem 2. Write a Hoare logic proof (decorated program) to show that the given Hoare triple holds and the program always terminates (hint: what is a ranking function?).
{x ≥ 0 ∧ y > 0} int r = x; int q = 0; while (y <= r) { r = r - y; q = q + 1;
}
{x = qy + r ∧ 0 ≤ r < y}
1
2
3
4
5
6
7
8
Problem 3. Consider the following program for sorting an array. Write a Hoare logic proof to prove the given Hoare triple, where sorted(a1,a2,...,ak) means a1 ≤ a2 ≤ ··· ≤ ak.
{0 ≤ N} int i = 1; while (i < N) { int j = i ;
while (j > 0 && A[j-1] > A[j]) { int t = A[j-1];
A[j-1] = A[j]; A[j] = t;
j = j - 1;
}
i = i + 1;
}
{sorted(A[0],A[1],A[2],...,A[N − 1])}
1
2
3
4
5
6
7
8
9 10
11
12
13
1
Turning in
• Create a private project with name homework4 in https://csed332.postech.ac.kr. Upload a scanned copy (or a typewritten document) of your answers in PDF format to homework4.
2
