Very nice! I always struggled with binary search programming problems until I starting frame things in a similar way: Check a certain condition, return the appropriate answer when it's false, write a guaranteed-to-terminate loop that maintains that same condition as an invariant, then interpret the final state to return the appropriate answer.