“Nondeterministic Relational Semantics of a while Program”, JAM, vol. 3, no. 3, pp. 242–260, Oct. 2013, doi: 10.24297/jam.v3i3.7222.