Seems trivial to me for infinite loops. Nothing special to specify here, they're already specced by the definition of loops.