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 179
- Downloads 0
Some class of generalized entire sequences of Modal Interval numbers
The history of modal intervals goes back to the very first publications on the topic of interval calculus. The modal interval analysis is used in Computer graphics and Computer Aided Design (CAD), namely the computation...
Full-Discrete Weak Galerkin Finite Element Method for Solving Diffusion-Convection Problem.
This paper applied and analyzes full discrete weak Galerkin (WG) finite element method for non steady two dimensional convection-diffusion problem on conforming polygon. We approximate the time derivative by backward fin...
Hermite Lagrange Interpolation on the Unit Circle
In this paper, we consider explicit representations and convergence of Hermite- Lagrange Interpolation on two disjoint sets of nodes, which are obtained by projecting vertically the zeros of (1- x2) Pn (?...
Quasi-Compactness in Quasi-Banach Spaces
Quasi-compactness in a quasi-Banach space for the sequence space Lp, p< 0 < p <1 has been introduced based on the important extension of Milman's reverse Brunn-Minkowiski inequality by Bastero et al. in 199...
Mathematica Module for Singularity Free Computations of Euler Parameters
In this paper,a Mathematica module for singularityfree computations of Euler parameters was established .The basic idea that we follow in developing these computationsis to make the values o...