摘要：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 inasmuch 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 firstorder predicate logic. Every proof is based on deriving the validity of some S-formula,so the procedure may be automated using automatic theorem provers. In this paper we will use Coq.
