From operational to denotational demonic semantics of nondeterministic while loops
Fairouz Tchier · Annual Conference on Computers · 2006
In this paper, we show that the operational semantics of a nondeterministic while loop give in previous paper is equal to the denotational one, which is given as the greatest fixed point of the semantic function Q ∨ P □ X in the demonic semilattices. As an intermediate result we give a generalization of the while statement verification rule of Mills.