Note that object-oriented programming is founded on the possibility for nonstandard interpretations: perhaps you have some code which is given a list of Objects, and you proceed to call the method toString on each of them. Certainly there is a standard interpretation for the function Object.toString, but your code is built to work even when you call this function and some nonstandard, custom, overridden method is called instead.
It can become very difficult to reason about programs when the run-time method invoked might be different from the one being called. We're used to speciflying type constratins which any interpretation must satisfy; wouldn't it be nice to specify more complicated constraints, e.g. "this function returns an int which is a valid index into [some array]"? And if we can describe the constraint formally (rather than in English comments, which is how most code works), then we could have the computer enforce that contractl (for every interpretation which gets executed, including non-static ones).
An obvious formal specifcation language is code itself have code which verifes pre-conditions before calling a function, and then runs code veriflying the post-condition before leaving the function. Indeed, there are several such tools about (Java , Scheme ). In the presence of inheritance, it's harder than you might initially think to do this correctly .
It is still a research goal to be able to (sometimes) optimize away such run-time verifications; this requires proving that some code is correct (at least, with respect to its post-condition). The fact that the code might call a function which will be later overridden (our "non-standard interpretations") exacerbates this difficulty. (And proving correctness in the presence of concurrency is even tougherl)
Even if not proving programs correct, being able to specify contracts in a formal language (code or logic) is a valuable skill.
- 1091 reads
