Logic programming tools and techniques for imperative program verification. - I. M. O'Neill (1987)