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 178
- Downloads 0
Predicting Assignment Submissions in a Multiclass Classification Problem
Predicting student failure is an important task that can empower educators to counteract the factors that affect student performance. In this paper, a part of the bigger problem of predicting student failure is addressed...
Comparison of Feature Selection Techniques in Knowledge Discovery Process
The process of knowledge discovery in data consists of five steps. Data preparation, which includes data cleaning and feature selection, takes away from 60% to 95% total time of the whole process. Thus, it is cruci...
Possibility to Increase Biofuels Energy Efficiency used for Compression Ignition Engines Fueling
The paper presents the possibilities of optimizing the use of biofuels in terms of energy efficiency in compression ignition (CI) engines fueling. Based on the experimental results was determinate the law of variat...
Diagnosis of the Potential for Successful Implementation of a Knowledge Management System in a University Unit member
This paper presents an overview of the recorded state in terms of the capacity for introducing of an informatics system for knowledge management of an academic institution – the Faculty of Administration and Information...
Backgrounds of Aggregated Assessment of SMEs Competitive Advantage Determinants
The study deals with the aggregated assessment of SMEs competitive advantage determinants in selected countries based on multiple criteria assessment methodology, in particular, Simple Additive Weighting (SAW), Com...