Ubiquitous Computing and Communication Journal
Disseminator of Knowledge
Home Home | About Us About Us | Contact Us Contact Us | Login Wednesday, April 1, 2020
Title: Least and greatest fixed points of a while semantics function
Authors: Dr. Fairouz Tchier
The meaning of a program is given by specifying the function (from
input to output) that corresponds to the program. The denotational
semantic definition, thus maps syntactical things into functions. 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 ({\it demonic relational semantics}). In this paper, we
concentrate on while loops. We will present some interesting results
about the fixed points of the while semantics function; $f(X)=Q\join
P\dcomp X$ where $\ldo{P}\meet \ldo{Q} =\Vide$, by taking
$P:=t\dcomp B$ and $Q:=\monocpl{t}$, one gets the demonic semantics
we have assigned to while loops in previous papers. We will show
that the least angelic fixed point is equal to the greatest demonic
fixed point of the semantics function.