Electronic Resource
Springer
Acta informatica
11 (1979), S. 195-210
ISSN:
1432-0525
Keywords:
PASCAL
;
Axiomatic definition
;
Program verification
;
Bounded machines
;
Clean termination
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract 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”.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF00289066
Permalink
|
Location |
Call Number |
Expected |
Availability |
