ResearchBib Share Your Research, Maximize Your Social Impacts
Sign for Notice Everyday Sign up >> Login

Formalization of the General Hoare Logic Laws

Journal: TEM JOURNAL - Technology, Education, Management, Informatics (Vol.1, No. 3)

Publication Date:

Authors : ;

Page : 145-150

Keywords : Program verification; program correctness; Hoare logic; first-order predicate logic; Coq.;

Source : Downloadexternal Find it from : Google Scholarexternal

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 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 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. In this paper we will use Coq.

Last modified: 2012-09-05 06:47:56