Abstract :
This paper formally describes a technique for proving that computer programs will always execute correctly. In order to do this, an abstract model for a program and its execution is given. Then, correctness of programs and proofs of correctness of programs are defined with respect to that model.
Keywords :
Abstract programs, debugging, program correctness, program execution model, state vector, theory of programming.; Computational modeling; Computer aided instruction; Debugging; Testing; Abstract programs, debugging, program correctness, program execution model, state vector, theory of programming.;
