C.M. Holt
University of Newcastle upon Tyne. 1994
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.