Browse by author
Lookup NU author(s): Dr Christopher Holt
An important reason that program verification is not widespread is that proofs tend to be much larger than both specifications and programs. The size of a proof is reduced if the languages used for specification, programming, and verification are similar (preferably identical). Visual programming languages have not generally been designed with specifications in mind, and visual specification languages have not generally been designed with programming in mind; this has hindered efforts to verify visual programs. An attempt has been made to rectify this by introducing visual predicates and inference rules to viz, a declarative visual language. An interpretation of line-and-box operations is offered in which the empty box, containing no successful evaluations of propositions, represents the false truth value, and every successful (i.e. non-empty) box is true. Unlinked boxes succeed independently, so their truths are disjoint, while linked boxes are mutually dependent for success, so their truths are conjoint. There is a test for failure, but negation is only introduced when relating propositions or values, e.g. via implication, so that the negation of failure is never constructed as a value. The language is illustrated by looking at the verification or a recursive insert sort algorithm.
Author(s): Holt CM
Publication type: Report
Publication status: Published
Series Title: Department of Computing Science Technical Report Series
Year: 1994
Pages: 16
Print publication date: 01/01/1994
Source Publication Date: 1994
Report Number: 482
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/482.pdf
