Axiomatic approach to total correctness of programs

purl.stanford.edu/bg513mr2075