sbv: 用SMT求解器验证程序-1

April 8, 2013

假设你要写一个函数，向一个有序（非递减）列表插入一个新元素，要求结果列表仍然有序。实现不难，但是你要怎样保证你的实现是正确的？

一般的单元测试

测试先行，先要先一个测试:


import Test.HUnit

test1 = TestCase $ do
    assertEqual (insert 9 []) [9]
    assertEqual (insert 1 [2, 3]) [1, 2, 3]
    assertEqual (insert 3 [1, 2]) [1, 2, 3]

运行这个测试，自然会出错，因为insert方法还没实现呢，所以你要编码实现一个insert，然后再运行测试。当测试最终通过的时候，一定程度上，我就可以相信你的实现是对的。

但是上面的这个测试有一个问题，test1只测试了一小部分可能输入，而且是固定的。对其他输入，你的实现会不会出错呢，谁也没法保证，说不定你就写了刚好能满足测试的insert。所以有Dijkstra的名言：Testing shows the presence, not the absence of bugs。

基于性质的测试

首先insert应改同时满足这些性质：

  1. 结果列表是有序的
  2. 结果列表是新元素和原列表的一个置换

分别用一个函数来表示这些性质：

import Test.QuickCheck

isSorted :: Ord a => a-> OrderedList a -> Bool
isSorted x (Ordered ls) = insert x ls == sort (x : ls)

isPermutationOf :: Ord a => a -> OrderedList a -> Bool
isPermutationOf x (Ordered ls) = sort (x:ls) == insert x ls

在一般的单元测试，我们也可以这么做，然后自己写几个用例。但是在基于性质的测试里，测试框架可以根据性质自动生成用例。

根据性质生成测试用例这点已经把一般的单元测试甩出了几条街，但毕竟还是测试，你只能多运行几次，生成多点测试用例来增加你的对insert的信心。

依赖类型

Curry–Howard同构说类型和命题之间、程序和证明之间存在对应关系，所以如果类型系统足够强悍，就能用一个类型表达出insert的性质，只要insert的实现符合这个类型，你就相当于证明了你的insert是对的。

这里有个两个前提：

  1. Curry–Howard同构的正确性
  2. 支持依赖类型的语言

用依赖类型就想写证明，性质一复杂我就晕掉，insert的第二个性质我现在还写不出来，第一个性质可以看Haskell入门。

使用SMT求解器

测试用例的不能覆盖全部输入，写证明又太复杂，如果能自动证明函数的性质那就好了。某天我发现了sbv，sbv可以用SMT求解器来验证程序的性质。而且有很多例子，看起来很诱惑。

然后我照着例子，把上面第一个性质用sbv写，然后对长度10的列表的插入进行验证，半个钟头没结果。要么是我写的太烂了，要么是求解器在穷举。