NQTHM proving sequential programs
Wim H. Hesselink · 1994
This is a presentation of the application of the theorem prover NQTHM of Boyer and Moore to correctness proofs of imperative programs in the style of programming methodology. Predicates and programs are represented syntactically. The interpretation is based on NQTHM's interpreter eval$. A library is constructed for the interpretation and proofs of while-programs, possibly with array modification. Linear search and a regrouping algorithm for arrays are provided as examples.