Proving correctness of programs in functional languages 
Author Message
 Proving correctness of programs in functional languages


Quote:
>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



Sat, 30 Oct 1993 03:19:11 GMT  
 Proving correctness of programs in functional languages
Dave Gillett:
        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 is nice, not only for "proof of correctness", but for things like
designing optimizers.  I believe everybody is familiar with the way a
specific case can often be implemented more efficiently than a general
case?

        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.

yacc at its finest :-)

The way I understand it, the term "functional language" was invented
by Backus to describe the deficiencies he saw in the languages he'd
helped develop (fortran, algol). Since people don't talk about this
much, I should point out that he also talked about Applicative State
Transition systems (with formal functional programming as the
subsystem used to generate a state).

Raul Rockwell



Sat, 30 Oct 1993 12:42:35 GMT  
 Proving correctness of programs in functional languages

]     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.

This has nothing to do with the distinction between functional
languages and procedural languages.  You have to have a meaning
function from the text to the semantic domain for any kind of
language.  If functional-language proofs don't discuss this, then it
is just because the writers are being sloppy about the distinction
between syntax and semantics.  Actually though, all the semantics I
have seen for functional languages _do_ address these issues.

The syntactic issues of many procedural languages are complicated by
type declarations, maybe that is what you are thinking of.  But the
existence of type declarations is orthogonal to the mechanism of the
language (functions, procedures, or predicates).  You can have a
functional language with type declarations and a procedural language
without them.

The apparent semantic simplicity of functional languages is an
illusion created by the fact that the functional languages whose
semantics have been described are just simple languages.  I can define
a procedural language that parallels the lambda calculus.  It has the
same number of basic forms and the semantics is no more complex.

If you want to compare the "semantic simplicity" of different
paradigms you just can't compare Pascal to FP, nor Turing Machines to
the lambda calculus.  You have to compare languages with the same
expressiveness and the same limitations.
--
                                        David Gudeman

noao!arizona!gudeman



Sat, 30 Oct 1993 14:12:49 GMT  
 
 [ 3 post ] 

 Relevant Pages 

1. Proving correctness of programs in functional languages

2. proving program correctness

3. Proving correctness of digital designs (H.G Barrow, 1984)

4. Concept Languages (was:Re: Paper Available: Theorem Proving, Concept Languages)

5. Is C a functional programming language?

6. Functional programming languages & formal verification

7. Sigma, an interpreted functional programming language implemented in C++

8. Macros in functional programming languages

9. optimizing interpreters for functional programming languages

10. Learning a functional programming language

11. literate programming and functional languages

 

 
Powered by phpBB® Forum Software