Formalization of the General Hoare Logic Laws
Journal Title: TEM JOURNAL - Year 2012, Vol 1, Issue 3
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.
Authors and Affiliations
Aleksandar Kupusinac, Dusan Malbaski
Keywords
Related Articles
- EP ID EP156110
- DOI -
- Views 185
- Downloads 0
Application of Skype API to Control Working Time
The purpose of this article is to present an innovative approach to monitor and control working time. A special software program is developed by Delphi implementing Skype API functions. This article shows three dif...
Mode of getting Thermal Energy Depending of the Average Outside Temperature on the City of Bitola
This research was based on the latest achievements in the development of energy technologies, such as: efficiency, energy saving, ecology and flexibility. The study used data from the measurements of external tempe...
A Fully Personalized Adaptive and Intelligent Educational Hypermedia System for Individual Mathematics Teaching-Learning
In this study, architecture and development process of UZWEBMAT, an adaptive and individualized environment based on learning styles and supported with expert system, are presented. UZWEBMAT was deve...
The Measurement of Hardness and Elastic Modulus of non-Metallic Inclusions in Steely Welding Joints
Trunk pipelines work under a cyclic dynamical mechanical load because when oil or gas is pumped, the pressure constantly changes - pulsates. Therefore, the fatigue phenomenon is a common reason of accidents. The fa...
Application of ICT in a Company after Identifying the Characteristics of a Crisis
The paper proposes the use of information and communication technology required to be applied in a company after identifying the characteristics of a crisis. This paper presents the internal and external causes of corpor...