A Hoare triple with imprecisely defined preconditions allows for a “weird” state change to occur. Tightening these preconditions by improving input checks would make these states unattainable.