QuickSort推导 - The Science of Programming

Posted on 2016-01-09 Edited on 2016-01-27

~~Edit~~

学习笔记 读书笔记 Programming

由于近日开发单片机程序的时候，写到一个小循环，不能确定其正确性，进而想到这本书的内容，算是一个小小的回顾。本书的读书笔记参考这篇The Science of Programming。
正所谓温故而知新，这次重新摘读又有些新的收获。本想以QuickSort作为一个练习来运用本书的知识，结果尝试了许久，发现越陷越深。最后还是找了书上的例子（书中有QuickSort的例子）。本文最终目标是阐述如何推导QuickSort程序本身。先摘取一些重要的知识点,再利用这些知识点来推导QuickSort。

QuickSort推导 - The Science of Programming
- 知识点梳理
- 推导Quick Sort （原书18.2节）
  - Partition （原书练习16.5）
  - Sort
    - 推导
    - C代码

知识点梳理

1. Quantification（量化）[原书4.2节]

There exists
(E i: mi\<n: E_i)
For all
(A i: mi\<n: E_i)
Numerial
(N i: mi\<n: E_i)

他们有以下特性

(E i: mi\<k+1: E_i) = (E i: mi\<k: E_i) V E_k+1
(A i: mi\<n: E_i) = (E i: mi\<n: E_i)
(E i: mi\<n: E_i) = (N i: mi\<n: E_i) 1
(A i: mi\<n: E_i) = (N i: mi\<n: E_i) = n-m

2. 何为wp？[原书第7章]

原书的定义：

The Predicate Transformer wp
The set of all states such that execution of S begun in any one of them is guaranteed to terminate in a finite amount of time in a state satisfying R.

wp通常被用来表达一段程序

或者这样写

Q:前条件
S:执行代码（原文称为commands）
R:后条件

wp的特性

1) wp(S,F) = F
2) wp(S ^ Q) ^ wp(S,R) = wp(S,Q ^ R )
3) if Q then wp(S, Q ) wp(S, R)
4) wp(S wp(S, R)) wp(S ,Q v R)
5) wp(S, Q) V wp(S, R) = wp(S, Q V R) (for deterministic S)

3. 循环检查 (原书第11章)

定义

用数学语言标记一个循环如下:
{Q}
{inv P: the invariant}
{bound t: the bound function}
{init IS: initialization command}
do B₁ S₁

B_n S_n
od

Invariant

A predicate P that is true before and after each iteration of a loop.

这就是说P在任何情况下都要成立，于是有

Q wp(IS, P)
P wp(DO, P ^ BB)

Bound

又叫bound function

The function changes at each iteration; the relation remains invariantly true.
each iteration decreases t by at least one，so that termination is guaranteed to occur.

检查bound函数确保循环能结束。

Checklist

非常重要!!!

Q wp(IS, P)
P ^ B_i wp(S_i, P)
P ^ BB R
P ^ BB (t > 0)
P ^ B_i wp(“t₁:=t; S_i“, “t < t₁“)

依次验证这5条，就能证明一个循环的正确性了

4. 如何运用所有的知识来开发一段程序（原书PART III）

推测Command

通过后条件R，来推测执行代码(Command)。这就是所谓的Programming as a Goal-Oriented Activity。详情参看原书第14章。

Strategy for developing an alternative command: To invent a guarded command，find a command C whose execution will establish postcondition R in at least some cases; find a Boolean B satisfying Bwp(C,R) and put them together to form B C. Continue to invent guarded commands until the precondition of the construct implies that at least one guard is true. - 原文(14.7)

获得Guard（原书第15章）

所有的编程都应该是结果导向的（这与测试驱动开发TDD的思想暗合）。所以后条件R是最先有的。
其次，通过P BB R能得到BB（即guard）。虽然有公式AB <=> A V B=T，但是B的获得感觉更多是依靠分析而不是推导。具体例子会在本文最后推导Quick Sort中提及。
其中

不过由上式可知，此时的guard还是个总的guard，还需要将之分解为各个B_i。

获得不变量Invariant（原书第16章）

书中给了4种方法：

Delete a conjunct. For example, predicate A ^ B ^ C can be weakened to A ^ C
Replace a constant by a variable. For example, predicate x b[1:10], where x is a simple variable，can be weakened to x b[1:i] ^ 110，where i is a fresh variable. Since a new
variable has been introduced, its possible set of values must be precisely stated.
Enlarge the range of a variable. For example, predicate 5 i < 10 can be weakened to 0 i < 10.
Add a disjunct. For example, predicate A can be weakened to A v B, for some other predicate B.

书中推荐用前三个，根据阅读本书后面部分的经验，最常用的还是第二条。

q++
p–
swap(b[p], b[q])
所以现在程序形式如下：
do pq-1
　if__ p:=p-1
　 __ q:=q+1
　 __ swap(b[p], b[q])
　fi
od

由command+P+BB获得Guard

PBBwp(S,P)

S = “p:=p-1”
　　wp(S,P) =
S = “q:=q+1”
过程类似
　　wp(S,P)=

对于前半部分的证明如下：
P中有
BB = (pq-1)
q < p q p-1 q+1p
得证
对于后半部分，显而易见需要b[q]x,即

swap(b[p], b[q])
　　wp(S,P)=

验证

Q: T
R:

wp(IS, P) =
PBB wp(,P)
这个显然也是成立的，因为我们的就是这么来的
PBBR
同上，亦成立
PBB(t>0)
BB = (pq-1) p-q+10
又由P有
qp+1 p-q+10
t=p-q+1>0
得证
P wp(“”, “t<t1")
对于三种,t都显然会变小，所以满足

综上，5条check point都满足，程序正确性可保证

Sort

推导

根据快速排序算法可知，对数组排序，即进行若干次分割，直至子区间包含2个元素，即可以进行直接排序。

P: s is a set of pairs (i, j) representing disjoint array sections b[i:j] of b. Further，b[0:n—1] is ordered iff all the disjoint partitions given by set s are.
IS: s:={(0,n-1)}
R: b[0:n-1] are ordered
t: n - ordered

快速排序程序如下:
s:={(0,n-1)}
{Invariant: 如上P}
do s{} Choose((i,j),s); s:=s-{(i,j)};
　　　if j-i \< 2 Sort b[i:j] directly
　　　 j-i 2 Partition(b,i,j,p;);
　　　fi
od

C代码

最终Quick Sort C代码实现如下:

1.#define N           50
2.#define MAX_SPLIT   50 // This should be logN
3.void swap(int* b, int p, int q)
4.{
5.    b[p]=b[p]+b[q];
6.    b[q]=b[p]-b[q];
7.    b[p]=b[p]-b[q];
8.}
9.int Partition (int* b, int m, int n)
10.{
11.    assert(n>m);
12.    int p=n-1, q=m+1;
13.    while (p != q-1)
14.    {
15.        if (b[p]>x)
16.        {
17.            p--;
18.        }
19.        else if (b[q]<=x)
20.        {
21.            q++;
22.        }
23.        else if (b[q]<=x && b[p]>x)
24.        {
25.            swap(b, p ,q);
26.            p--;
27.            q++;
28.        }
29.    }
30.    return p;
31.}
32.void QuickSort(int* b, int n)
33.{
34.    typedef struct 
35.    {
36.        int start;
37.        int end;
38.    }Pair s[MAX_SPLIT] = {0};
39.    int count = 1; // how many pairs in s
40.    s[0].start = 0;
41.    s[0].end = n-1;
42.    while (count > 0)
43.    {
44.        Pair p;
45.        memcpy(&p, &s[count-1], sizeof(Pair));
46.        if(p.end - p.start < 2)
47.        {
48.            if (p.start > p.end)
49.            {
50.                swap (b, p.start, p.end);
51.                count --;
52.            }
53.            else
54.            {
55.                int m = p.start;
56.                int n = p.end - p.start + 1;
57.                int x = Partition(b, m, n);
58.                s[count-1].start = p.start;
59.                s[count-1].end = x-1;
60.                s[count].start = x+1;
61.                s[count].end = p.end;
62.                count ++;
63.            }
64.        } 
65.    }
66.}

Big Ben