|
|
|---|
|
|
|
|---|
B. Brock and J S. Moore, “A
Mechanically Checked Proof of a Comparator Sort Algorithm”, in
M. Broy, J. Gruenbauer, D. Harel, and C. A. R. Hoare, editors,
Engineering Theories of Software Intensive Systems, Springer NATO
Science Series II, 195, pp. 141-175, 2005.
Relevance: an example of proving that the state
transformation effected by running a CAP model on commercial microcode
implements the high level specification
Abstract
We describe a mechanically checked correctness proof for the comparator sort algorithm underlying a microcode program in a commercially designed digital signal processing chip. The abstract algorithm uses an unlimited number of systolic comparator modules to sort a stream of data. In addition to proving that the algorithm produces an ordered permutation of its input, we prove two theorems that are important to verifying the microcode implementation. These theorems describe how positive and negative “infinities” can be streamed into the array of comparators to achieve certain effects. Interesting generalizations are necessary in order to prove these theorems inductively. The mechanical proofs were carried out with the ACL2 theorem prover. We find these proofs both mathematically interesting and illustrative of the kind of mathematics that must be done to verify software.
For the 1997 ACL2 proof script see
See the discussion of the CAP DSP project in operational-semantics-2__other-examples.