Abstraction in program verification. - John T. Latham (1985)