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 175
- Downloads 0
The Effects of Total Quality Management Practices on Performance within a Company for Frozen Food in the Republic of Macedonia
The subject of this paper is designing and implementation of the TQM philosophy within a frozen food company which deals with processing, manufacturing, distribution and sale of products from snails which is exclus...
Stratified Charge Flame Ignite in a Gasoline Engine Conform to the Engine Operating Regimes of Indicator of Combustion Characteristics and Burn Time and their Empirical Equations
Past and present, there are many studies related to the internal combustion engine to improve performance, reduce fuel consumption and emissions. In the literature, in order to increase the efficiency of engine com...
Metamodel of the REA model level
This paper describes the gradual formation of the metamodel of the REA model level of the REA enterprise ontology. The paper aims to create a basic structure that allows creating valid models of the ontology. The f...
A New Perspective: Organizational Citizenship Behaviour and its Reflections
Organizational citizenship behaviour is not only confined to the behaviours of the organizational workers in accordance with the definitions of their roles, but it also includes all the other behaviours they di...
Computational Fluid Dynamics (CFD) Analysis for Predicting the Airflow in a Data Centre
This paper studies the high density data centre with 266.4 m2 area, and it focuses on defining the heat profile of the centre, as well as on the airflow in the centre. To this purpose, the necessary measurements in the d...