This monograph deals with aspects of the computer programming
process that involve techniques derived from mathematical logic.
The author focuses on proving that a given program produces the
intended result whenever it halts, that a given program will
eventually halt, that a given program is partially correct and
terminates, and that a system of rewriting rules always halts.
Also, the author describes the intermediate behavior of a given
program, and... more...