Formalization of the general rules of the Hoare logic using S-formulas

In this paper we present an approach to formalizing the general rules of the Hoare logic that 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. The general rules of Hoare logic, such as the rules 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 may be automated using automatic theorem provers, such as Coq.