Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!wuarchive!uunet!futures!saxony!dgil
From: dgil@pa.reuter.COM (Dave Gillett)
Newsgroups: comp.lang.misc
Subject: Proving correctness of programs in functional languages
Message-ID: <873@saxony.pa.reuter.COM>
Date: 13 May 91 19:19:11 GMT
Distribution: na
Organization: Reuter:file Inc  (A Reuter Company) Palo Alto, CA
Lines: 33

In <ROCKWELL.91May10205204@socrates.umd.edu> rockwell@socrates.umd.edu (Raul Rockwell) writes:

>This is related to proving a program correct.

>I should note that functional languages seem to be rather promising
>in this regard.


     I consider that an extreme understatement.

     When we define our domain of discourse to be functions, which accept
inputs and produce (we hope!) results, we are able to express the necessary
properties for verification of each function in terms of predicates linking
properties of the inputs to properties of the results.  Composition of
functions leads to combination and simplification of intermediate predicates,
and ultimately to the set of pre- and post-conditions which demonstrates (or,
as appropriate, fails to demonstrate) that our composition has the properties
which we wish it to have.

     This exercise is entirely in terms of functions and predicates, which are
mathematical objects, and any well-defined functional notation is sufficient to
allow us to proceed to proof.

     By contrast, the majority of the literature that I have seen on the
verification of procedural programs starts, instead, from the notion that
a program is a "text".  Resolution of syntactic and semantic issues, in order
to arrive at suitable objects for reasoning, becomes a major task; indeed, there
is rarely time or space left for the actual proof itself.

     Formal methods are capable of great (but not infinite!) power.  But it
seems to me that they are, so far, only practical when applied to a functional
context.
                                                     Dave