Formalization of the General Hoare Logic Laws
Formalization of the General Hoare Logic Laws

Summary/Abstract: This paper presents a new approach to formalizing the general rules of the Hoare logic. Our way is based on formulas of the first-order predicate logic defined over the abstract state space of a virtual machine, i.e. so-called S-formulas. S-formulas are general tool for analyzing program semantics in as much as Hoare triples of total and partial correctness are not more than two S-formulas. The general rules of Hoare logic, such as the laws of consequence, conjunction, disjunction and negation can be derived using axioms and theorems of first order predicate logic. Every proof is based on deriving the validity of some S-formula, so the procedure maybe automated using automatic theorem provers. In this paper we will use Coq.

• Details
• Contents