First-order logic applied to the description and derivation of programs
P. E. Vasey · Spiral (Imperial College London) · 1985
Automating the process of programming has been a m a jor goal of scientists ever since the advent of electronic computers.In this dissertation w e pursue a modus operandi in which errors caused by human fallibility, whether logical or clerical, can never contribute to the production of incorrect code.This modus operandi for producing such robust and reliable software is based upon the language of First-Order Predicate Logic (FOPL) and the following methodology :-1.The initial and most crucial stage is the writing of informal and then formal specifications which capture the intended concepts of a problem.2. By reasoning about a set of axioms which constitute a formal specification, theorems can be derived which form an inherently correct logic program."... the mathematics of com putation may have, as one of its major aspects, rules which permit us to transform functions from a non-computable form into a computable form.""It is a great nuisance that knowledge can only be acquired by hard work.It would be fine if we could swallow the powder of profitable information made palatable by the jam of fiction.