Two Weak Links in the Formal Methods Chain

ification of programming languages and cryptographic protocols. It is sometimes thought that a language such as C is not sufficiently well-specified to support formal proofs. However, this is only a part-truth. A bigger problem is that the specification leaves so many possibilities open that proofs of properties from a corresponding formal specification would be quite difficult. For instance, the following correct C++ program void main()-- int a[] = --1,2,3; for (int i = 0; i ! 3; i++) -- a[i-1] = -1; cout !! "i = " !! i !! ", "; Author email addresses: fgunter,lee,scedrovg@cis.upenn.edu. has the output i = -1, i = -1, ... for at least one machine, compiler, and program run, because its semantics depends on the runtime layout of the variables. 1 By contrast, it is easier to formulate properties for a more restrictive design, if there is a sufficiently rigorous specification. For instance