《Parameterized Unit Tests》：

Parameterized unit tests extend the current industry practice of using closed unit tests defined as parameterless methods. Parameterized unit tests separate two concerns: 1) They specify the external behavior of the involved methods for all possible test arguments. 2) Test cases can be re-obtained as traditional closed unit tests by instantiating the parameterized unit tests. Symbolic execution and constraint solving can be used to automatically choose a minimal set of inputs that exercise a parameterized unit test with respect to possible code paths of the implementation. In addition, parameterized unit tests can be used as symbolic summaries which allows symbolic execution to scale for arbitrary abstraction levels. We have developed a prototype tool which computes test cases from parameterized unit tests; it is integrated into the forthcoming Visual Studio Team System product. We report on its first use to test parts of the .NET base class library.

相關連結：

我覺得 skybrain 說得比較好：

The major reason why unit tests are popular in commercial settings, while proofs aren't, is that unit tests are much easier to understand, precisely because they have such a low level of abstraction. Raising the level of abstraction is going in the wrong direction - the unit test will be no easier to understand than the code it tests.

不過，我覺得這類的技術，應該用在 assertion 上，用 proof 的方式，驗證 pre-condition 與 post-condition。