Browse by author
Lookup NU author(s): Dr Christopher Holt
Full text is not currently available for this publication.
One reason for the popularity of declarative languages is the reduction in distance between thinking about mathematical specifications and programming algorithms. This makes formal reasoning about programs easier; and one view holds that a programming language should be an executable subset of a specification language, so that the source and target languages of a proof are identical. A natural extension of this approach is to extend the domain of a language to include proofs; then, verification can be done entirely within the same linguistic environment. A problem that arises is the sheer size of proofs; they seem to be an order of magnitude larger than either specifications or programs. This difficulty can be mitigated by making the application of rules of inference implicit, but clear enough that a very simple-minded proof checker can derive them. The use of a visual language seems to enhance the clarity of annotations that hint at formal, explicit proofs; this is illustrated with the traditional examples of a sort and a stack.
Author(s): Holt CM
Publication type: Report
Publication status: Published
Series Title: Department of Computing Science Technical Report Series
Year: 1993
Pages: 44
Report Number: 436
Institution: Department of Computing Science, University of Newcastle upon Tyne
Place Published: Newcastle upon Tyne
URL: http://www.cs.ncl.ac.uk/publications/trs/papers/436.pdf
