The Design of Functional Programs - A Calculational Approach

This document shows to what extent functional programs can be designed in a calculational way. This study is about programming, as a design activity; it is not about programming languages, formal semantics included, nor about implementations.

**Tag(s):**
Formal Methods

**Publication date**: 31 Dec 1989

**ISBN-10**:
n/a

**ISBN-13**:
n/a

**Paperback**:
n/a

**Views**: 13,548

**Type**: N/A

**Publisher**:
n/a

**License**:
n/a

**Post time**: 09 Oct 2006 02:25:16

The Design of Functional Programs - A Calculational Approach

This document shows to what extent functional programs can be designed in a calculational way. This study is about programming, as a design activity; it is not about programming languages, formal semantics included, nor about implementations.

John Pinto

Document Excerpts:

It is well-known that there is only one way to establish the correctness of a computer program, namely by rigorous mathematical proof. Acceptance of this fact leaves room for two possible approaches to programming. In the first approach, a program is constructed first and its correctness is proved afterwards. This approach has two drawbacks. First, for an arbitrary program it may be very difficult, if not impossible, to prove its correctness. Second, this approach sheds no light on the methodological question how programs are to be designed.

In the second approach, advocated and developed by E.W. Dijkstra and others, the program and its proof of correctness are constructed simultaneously. Here, the obligation to construct a proof of correctness is used as a guiding principle for the design of the program. When applied rigorously, this approach can never give rise to incorrect programs; the worst thing that can happen is that no program is constructed at all because the problem is too difficult.

This document was started as a research to what extent functional programs can be designed in a calculational way. This should be possible because functional-program notations carry less operational connotations than their sequential counterparts do, functional-program notations more resemble "ordinary" mathematical formalisms than sequential-program notations do. This raised a question of whether the two ways of programming are really different: they might very well turn out to have more in common than one would expect at first sight.

The results of this research are laid down in this document. This study is about programming, as a design activity; it is not about programming languages, formal semantics included, nor about implementations. This implies that this document discusses semantics and implementations only as far as needed for its purpose, namely the formulation of a set of rules for designing programs.

Document Excerpts:

It is well-known that there is only one way to establish the correctness of a computer program, namely by rigorous mathematical proof. Acceptance of this fact leaves room for two possible approaches to programming. In the first approach, a program is constructed first and its correctness is proved afterwards. This approach has two drawbacks. First, for an arbitrary program it may be very difficult, if not impossible, to prove its correctness. Second, this approach sheds no light on the methodological question how programs are to be designed.

In the second approach, advocated and developed by E.W. Dijkstra and others, the program and its proof of correctness are constructed simultaneously. Here, the obligation to construct a proof of correctness is used as a guiding principle for the design of the program. When applied rigorously, this approach can never give rise to incorrect programs; the worst thing that can happen is that no program is constructed at all because the problem is too difficult.

This document was started as a research to what extent functional programs can be designed in a calculational way. This should be possible because functional-program notations carry less operational connotations than their sequential counterparts do, functional-program notations more resemble "ordinary" mathematical formalisms than sequential-program notations do. This raised a question of whether the two ways of programming are really different: they might very well turn out to have more in common than one would expect at first sight.

The results of this research are laid down in this document. This study is about programming, as a design activity; it is not about programming languages, formal semantics included, nor about implementations. This implies that this document discusses semantics and implementations only as far as needed for its purpose, namely the formulation of a set of rules for designing programs.

Tweet

About The Author(s)

No information is available for this author.

No information is available for this author.

No information is available for this author.

Book Categories

Computer Science
Introduction to Computer Science
Introduction to Computer Programming
Algorithms and Data Structures
Artificial Intelligence
Computer Vision
Machine Learning
Neural Networks
Game Development and Multimedia
Data Communication and Networks
Coding Theory
Computer Security
Information Security
Cryptography
Information Theory
Computer Organization and Architecture
Operating Systems
Image Processing
Parallel Computing
Concurrent Programming
Relational Database
Document-oriented Database
Data Mining
Big Data
Data Science
Digital Libraries
Compiler Design and Construction
Functional Programming
Logic Programming
Object Oriented Programming
Formal Methods
Software Engineering
Agile Software Development
Information Systems
Geographic Information System (GIS)

Mathematics
Mathematics
Algebra
Abstract Algebra
Linear Algebra
Number Theory
Numerical Methods
Precalculus
Calculus
Differential Equations
Category Theory
Proofs
Discrete Mathematics
Theory of Computation
Graph Theory
Real Analysis
Complex Analysis
Probability
Statistics
Game Theory
Queueing Theory
Operations Research
Computer Aided Mathematics

Supporting Fields
Web Design and Development
Mobile App Design and Development
System Administration
Cloud Computing
Electric Circuits
Embedded System
Signal Processing
Integration and Automation
Network Science
Project Management

Operating System
Programming/Scripting
Ada
Assembly
C / C++
Common Lisp
Forth
Java
JavaScript
Lua
Microsoft .NET
Rexx
Perl
PHP
Python
R
Rebol
Ruby
Scheme
Tcl/Tk

Miscellaneous
Sponsors