<编程珠玑>笔记 程序验证

Posted 2020-06-28

  在芯片设计(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 

View Code

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; 

View Code

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) }

View Code

 

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
*/