Functional Specification and Verification of Object-Oriented Programs
One weakness of Hoare-style verification techniques based on first-order predicate logic is that reasoning is backward from post-conditions to preconditions. A natural, forward reasoning is possible by viewing a program as a mathematical function that maps one program state to another. This functional program verification technique requires a minimal mathematical background as it uses equational reasoning based on sets and functions. Thus, it can be easily taught and used in practice. In this paper, the authors formalize a functional program specification and verification technique and extend it for object-oriented programs. Their approach allows one to formally specify and verify the behavior of an object-oriented program in a way that is natural and closer to the way one reasons about it informally.