今天看了一点契约式设计（DBC）的介绍，按阅读顺序记录之。

1. Why I do Design by Contract

看完之后，有DBC就是往代码里插assert感觉。当然不能顺便插断言，例如在函数入口插的断言要检查输入（前置条件），在函数出口插的要检查输出（后置条件）。

和Unit test、TDD的比较：

1. 单元测试和实现代码分离，DBC里契约在实现代码中查（易查看，可以做文档）
2. 单元测试只能检查预先想到的一小部分输入，DBC可以一直检查（知道遇到错误然后挂掉）
3. 单元测试注重独立的模块

和Defensive programming不同，DBC里输入有错就抛异常或直接退出完事，而Defensive则要处理这些错误。当然只是我比较片面的理解。

实现Fibonacci数列来演示一下（不准确）：

一般的实现：

fib n
    | n == 1 = 1
    | n == 2 = 1
    | otherwise = fib (n - 1) + fib (n - 2)

Defensive的实现，处理非法输入：

fib n
    | n <= 0 = Nothing
    | n == 1 = Just 1
    | n == 2 = Just 1
    | otherwise = (+) <$> fib (n - 1) <*> fib (n - 2)

DBC的实现，遇到非法输入直接抛异常。

fib n
    | assert (n > 0) = error "n must larger than 0"
    | n == 1 = 1
    | n == 2 = 1
    | otherwise = fib (n - 1) + fib (n - 2)

2. D语言的DBC支持

接着看来D语言里的DBC。D语言对DBC有语法支持，一个函数可以分成in、out和body部分，分别对应前置条件、后置条件和实际的函数。有了这样的分块后，断言的使用就更加系统。

void func() {
  in {
    //asserts
  }

  out {
   //aserts
  }

  body {
    // function logic
  }
}

调用一个函数的时候按in -> body -> out的顺序执行，断言也是抛异常。

类里面可以有invariant()方法，用来检查不变量。

.Net

不太认真地看了.Net 4.0的DBC，没有语法支持，也是到处插断言，概念也多。

Liquid Haskell

上面各种实现更多是在运行时检查错误，Haskell自然也可以。Liquid Haskell实现了在编译时静态检查。使用Liquid Haskell要给Haskell函数写注释，然后用logic solver做验证。虽然这里完全没提到contract，但是前置、后置条件还是有的。准备读点论文再来看。