A Decision Procedure for the Correctness of a Class of Programs
Prabhaker Mateti · Journal of the ACM · 1981
Verification of certain properties of a class of programs is considered.The programs are written In a miniprogrammmg language that has variables of only two data types, a linear array of elements, and pomters to these elements.The array elements can only be exchanged; pointers can only be incremented or decremented by one Program properties to be venfied are expressed in a severely restricted assertion language which contains essentially Boolean expressions of comparisons among pointers and among array elements Several in-place sorting algorithms can be readily written and asserted m these languages A decision procedure for the truthhood of the verification conditions generated for the above class of asserted programs is presented An algorithm for generating counterexamples for false verification conditions is also given The theorem prover can be readily implemented using simple graph algorithms The objective of this exercise is to use problem knowledge to design simple and efficient verifiers.The techmques developed seem applicable to wider classes of programs mampulatmg data structures.