Once a program has been written, it can be checked against its specification either statically (i.e. program verification) or dynamically (i.e. testing). The project merges these techniques by assuming that assertions are always checked dynamically but optimizing away as many checks as possible. Thus, program verification becomes a special case of code optimization. Code optimization and program verification will be linked by using the specification for program components to optimize the programs that use them. Program components with specifications are likely to be faster than those without, thus encouraging programmers to specify them. The project will also study how to provide performance information so that the programmer can see how to add assertions to improve performance and can see when components are used incorrectly. The project will use the TS compiler for Typed Smalltalk and the mu-ral interactive theorem prover.
