A formalized proof system for total correctness of while programs : (preprint)
Jan Aldert Bergstra, Jan Willem Klop · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1981
We introduce datatype specifications based on schemes, a slight generalization of first order specifications.For a schematic specification o:~JE), Hoare's Logic HL(E,IB) for partial correctness is defined as usual and on top of it a proof system (E, lE ) Ip + S + for termination assertions is defined.The system is first order in nature, but we prove it sound and complete w.r.t. a second order semantics.We provide a translation of a standard proof system HLT(A) for total correctness on a structure A into our format.