F. Tchier, “Nondeterministic Relational Semantics of a while Program”, JAM, vol. 3, no. 3, pp. 242–260, Oct. 2013.