在芯片设计(IC)领域有专门的职位叫做芯片验证工程师，其中的一种方法叫形式验证(Formal Verification)，具体包括等价性检查，模型检查和定理证明。
本章所讲的程序验证方法(不要与软件测试混为一谈)，与芯片行业的形式验证法非常相似。参考芯片行业，随着分工的细化，软件也会有专门的验证工程师。
1 Binary search
determine whether the sorted array x[0..n-1] contains the target element t
mustbe(range): the key idea is that we always know that if t is anywhere in x[0..n-1], then it must be in a certain range of x
1) sketch
initialize range to 0..n-1
loop
{ invariant: mustbe(range) }
if range is empty,
break and report that t is not in the array
compute m, the middle of the range
use m as a probe to shrink the range
if t is found during the shrinking process
break and report its position
2) refine
lo = 0, up = n-1
loop
{ mustbe(lo, up) }
if lo > up
p = -1; break
m = lo/2 + (up - lo)/2;
case
x[m] < t: lo = m + 1;
x[m] == t: p = m; break
x[m] > t: up = m -1;
3) program
1 { musbe(0, n-1) }
2 lo = 0; up = n-1
3 { mustbe(lo, up) }
4 loop
5 { mustbe(lo, up) }
6 if lo > up
7 { lo > up && mustbe(lo, up) }
8 { t is not in the array }
9 p = -1; break
10 { mustbe(lo, up) && lo <= up }
11 m = lo/2 + (up - lo)/2;
12 {mustbe(lo, up) && lo <= m <= up}
13 case
14 x[m] < t:
15 { mustbe(lo, up) && cantbe(0, m)}
16 { mustbe(m+1, up) }
17 lo = m +1
18 { mustbe(lo, up) }
19 x[m] == t:
20 { x[m] == t}
21 p = m; break
22 x[m] > t:
23 { mustbe(lo, up) && cantbe(m. n-1) }
24 { mustbe(lo, m-1) }
25 u = m-1
26 { mustbe(lo, up) }
27 { mustbe(lo, up) }
2 Program verification
1) assertions
inputs, variables, and output
2) sequential control structures
"do this statement and then that statement"
place assertions between them and analyze each step of the program‘ progress individually
3) selection control structures
"if", "case": one of many choices is selected
consider each of the several choices individually
4) iteration control structures
initialization: invariation is true when the loop is executed for the first time
preservation: invariation is true before and after each iteration of loop
termination: the desired result is true whenever execution of the loop terminates
5) functions
precondition: the state(inputs, variables) must be true before it is called
postcondition: what the function will guarantee on termination
int bsearch( int t, int x[], int n )
/* precondition: x[0] <= x[1] <= ... <= x[n-1]
postcondition:
result == -1 => t not present in x
0 <= result < n => x[result] == t
*/