Tchier, F. Nondeterministic Relational Semantics of a While Program. JAM 2013, 3, 242-260.