Hoare's Logic for Programming Languages with Two Data Types

摘要

The completeness of Hoare's logic is considered with a first order assertion language applied to while-programs containing variables of two (or more) distinct types. While Cook's completeness theorem generalities to many sorted interpretations certain fundamentally important structures turn out not to be expressive. The case of programs with distinguished counter variables and boolean variables adjoined is studied; for example, it is shown that adding counters to arithmetic destroys expressiveness.