Abstract: Traditional unit tests in test-driven development compare a few concrete example executions against the developer’s definition of correct behavior. However, a developer knows more about how a program should behave than can be expressed through concrete examples. These general insights can be captured as theories, which precisely express software properties over potentially infinite sets of values. Combining tests with theories allows developers to say what they mean, and guarantee that their code is intuitively correct, with less effort. The consistent format of theories enables automatic tools to generate or discover values that violate these properties, discovering bugs that developers didn't think to test for.
Subscribe to Posts [Atom]