This article, by Dr. Ben Brosgol, focuses on a mixture of formal methods and testing practices (together called “hybrid verification”) and the use of “contracts” that consist of preconditions and postconditions in order to formalize the assumptions made by critical code.

I chose to write about this article because it highlights some of the limits of testing, shows how to provide additional security for critical code, and introduces contact-based programming.

Brosgol defines a “contract” in programming as a set of preconditions and postconditions that wrap a subprogram (function, method, etc.) call.  The subprogram cannot begin unless its preconditions are met, and cannot return until its posconditions are true.  This provides a contract between a program and its subprograms that guarantees a certain state at critical times.  There are tools written for some languages (he uses SPARK as an example) that can do both static and dynamic contract testing and provide proof that the code will work as specified.

Brosgol then details ways to mix testing and formal verification.  If formally verified code calls subprograms that were tested rather than proven, the formal analysis tools will attempt to show that the preconditions are met, and assume that the tested code satisfies the postconditions.  This also requires that either the contracts are checked at runtime, or that sufficient testing was done such that the developer is confident the contracts will be fulfilled by the tested code.  If formally verified code is called from tested code, there need to be runtime checks for the preconditions (because the tested code does not guarantee those in the way the formal verification requires), but because the postconditions have been proven there is no need for checks at that point.

Next, Brosgol mentions the need for good choice of postconditions.  Strong, extensive postconditions make it easier to provide proof, but may have unacceptable overhead if they need to be checked dynamically.

He concludes that the relatively new combination of formal proof tools and contract verification on both a static and a dynamic basis opens up new avenues to create code that secures its critical sections.

This article helped me to understand that there’s a much wider world of testing beyond what we covered in class.  We didn’t talk about proof-based testing at all, and that’s a subject area that I believe I should learn more about.  It also highlights the way that our understanding of testing is ever-expanding.

From the blog CS@Worcester – orscsblog by orscsblog and used with permission of the author. All other rights reserved by the author.