Formalization of the General Hoare Logic Laws
Journal: TEM JOURNAL - Technology, Education, Management, Informatics (Vol.1, No. 3)Publication Date: 2012-09-01
Authors : Aleksandar Kupusinac Dusan Malbaski;
Page : 145-150
Keywords : Program verification; program correctness; Hoare logic; first-order predicate logic; Coq.;
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.
Other Latest Articles
- A survey on academic teachers’ perceptions about ICT in education
- Enhancing E-Mail Marketing by Semantic Addressing
- HEALTH STATUS OF ELDERLY WOMEN IN SOCIO-ECONOMIC AND CULTURAL CONTEXT IN PUNJAB, PAKISTAN
- AN ANALYSIS OF TECHNICAL, VOCATIONAL AND COMMERCIAL EDUCATION CONTRIBUTION TOWARDS FACULTY SATISFACTION IN TERMS OF ACADEMIC AND PROFESSIONAL DEVELOPMENT
- WOMEN IN AGRICULTURAL DECISION MAKING: PAKISTAN’S EXPERIENCE
Last modified: 2012-09-05 06:47:56