Reasoning about higher-order imperative programs
Sergey Vadimovich Kotov, Allen Stoughton · 1997
We consider the problem of formal reasoning about mainstream programming languages. Such languages include efficient direct store manipulations as well as higher-order constructions for structured programming. The interplay of store manipulations and higher-order functions invalidates most of the reasoning techniques developed for theoretical toy languages. The notion one wants to study is that of observational equivalence of incomplete pieces of code. This notion naturally arises in step-wise software development, program verification, program semantics, as an equivalence relation on fragments of code. Although extensively studied in the areas of functional programming and concurrency, the concept of observable equivalence lacks a theory applicable to imperative programming. Our approach consists of extending recent formal techniques from pure functional languages to imperative higher-order languages. We concentrate on a systematic development of the notion of simulation, a binary relation that approximates the observational equivalence from below. Several versions of this notion have been developed. We build a uniform framework for generating simulation relations for various programming languages and for establishing the congruence property of these relations.