Sign in
Demonic fixed point of semantics function
Conference proceeding

Demonic fixed point of semantics function

SERP '05: Proceedings of the 2005 International Conference on Software Engineering Research and Practice, Vols 1 and 2, pp.670-677
01/01/2005

Abstract

Computer Science Computer Science, Software Engineering Science & Technology Technology
We deal with a relational model for the demonic semantics of programs. In particular, we prove some relevant results about fixed points of functions that involve demonic operators. We give explicitly the expression of the greatest fixed point wrt to the demonic ordering (demonic inclusion) of the semantic function assigned to nondeterministic while loops in previous papers. We show that this greatest fixed coincides with the least fixed point wrt to the usual ordering (angelic inclusion) of the same function.

Metrics

1 Record Views

Details