Program Logic Without Binding is Decidable

Abstract

When the "binding mechanisms" of assignment, quantification, and procedure definition are removed from a conventional first order total correctness logic of programs, the remaining logical system is decidable in time approximately one exponential in the length of the input. This system is maximal in the sense that the presence of any one of the three binding mechanisms would make it undecidable. Such a decision procedure can play a central role in the construction of program verifiers based on decision methods.