That’s a well said example and actually very easy to establish formally by complementation. I don't really care if Hoare notation, the predicate calculus, or ev

That’s a well said example and actually very easy to establish formally by complementation. I don't really care if Hoare notation, the predicate calculus, or even English is the language of choice, so long as the argument is rigorous. That said we all know how difficult avoiding ambiguity is in English, so I wouldn’t choose it except for the broad strokes.