Nondeterministic Relational Semantics of a while Program
Journal Title: JOURNAL OF ADVANCES IN MATHEMATICS - Year 2013, Vol 3, Issue 3
Abstract
A relational semantics is a mapping of programs to relations. We consider that the input-output semantics of a program is given by a relation on its set of states; in a nondeterministic context, this relation is calculated by considering the worst behavior of the program (demonic relational semantics). In this paper, we concentrate on while loops. Calculating the relational abstraction (semantics) of a loop is difficult, but showing the correctness of any candidate abstraction is much easier. For functional programs, Mills has described a checking method known as the while statement verification rule. A programming theorem for iterative constructs is proposed, proved, demonstrated and applied for an example. This theorem can be considered as a generalization of the while statement verification to nondeterministic loops.
Authors and Affiliations
Fairouz Tchier
Keywords
Related Articles
- EP ID EP651204
- DOI 10.24297/jam.v3i3.7222
- Views 190
- Downloads 0
Approximation of The Lower Operator in Nonlinear Differential Games with Non-Fixed Time
Approximate properties of the lower operator in nonlinear differential games with non-fixed time are studied.
PSEUDO-SLANT SUBMANIFOLD IN KENMOTSU SPACE FORMS
In this paper, we study geometry of the pseudo-slant submanifold of a Kenmotsu space form. Necessary and suffcient conditions are given for a submanifold to be a pseudo-slant submanifold in Kenmotsu manifolds....
On a Subclass of Meromorphic Multivalent Functions
In this paper, we introduce a new class of meromorphic multivalent functions in the puncturedunit discU*{z∈c:0 <|z|<1} . We obtain various resultsincluding coefficients inequality, convex set, radius of sta...
Combined effects of Hall current and variable Viscosity on Non-Newtonian MHD flow past a stretching vertical plate
This paper investigate the effects of Hall currents on free-convective steady laminar boundary-layer flow, past a semi-infinite vertical plate, for large temperature differences . A uniform magnetic field is applied perp...
Cycles Cohomology and Geometrical Correspondences of Derived Categories to Field Equations
The integral geometry methods are the techniques could be the more naturally applied to study of the characterization of the moduli stacks and solution classes (represented cohomologically) obtained under the study of th...