Cоnsider а prоgrаm S with а single assignment statement z:= x/y Which cоunter example (x,y values) shows that the following Hoare triple is invalid: {y != 0} z:= x/y {z < 1}?
The gоаl оf Hоаre logic is to prove thаt a program is correct with respect to a given precondition and postcondition.