The clean termination of Pascal programs

The axiomatic definition of PASCAL takes no account of the finite bounds of real computers. It is proposed that the bounds of differing machines may be accounted for in the PASCAL definition by the use of an axiom schema with machine dependent parameters. If these parameters are available to the program prover and to the program it is possible to prove the clean termination of a program on a particular bounded machine. The use of a parameterised definition for all PASCAL machines, means that clean termination can be guaranteed over a range of machines. In particular a programmer may prove his program against a set of bounds chosen for ease of proof, as long as the implemented machine is larger.