Nondeterministic Relational Semantics of a while Program. JAM. 2013;3(3):242-260. doi:10.24297/jam.v3i3.7222