Reasoned Programming

Presents informal way of attempting a mathematical proof of reliability to make sure that our computer programs will work reliably. Also shows the benefits of the approach even without strict formality.

**Tag(s):**
Formal Methods

**Publication date**: 01 Jan 1994

**ISBN-10**:
n/a

**ISBN-13**:
n/a

**Paperback**:
n/a

**Views**: 13,253

**Type**: N/A

**Publisher**:
n/a

**License**:
n/a

**Post time**: 20 Sep 2006 07:55:09

Reasoned Programming

Presents informal way of attempting a mathematical proof of reliability to make sure that our computer programs will work reliably. Also shows the benefits of the approach even without strict formality.

Book Excerpts:

Can we ever be sure that our computer programs will work reliably? One approach to this problem is to attempt a mathematical proof of reliability, and this has led to the idea of Formal Methods: if you have a formal, logical specification of the properties meant by 'working reliably', then perhaps you can give a formal mathematical proof that the program (presented as a formal text) satisfies them.

Of course, this is by no means trivial. Before we can even get started on a formal proof we must turn the informal ideas intended by 'working reliably' into a formal specification, and we also need a formal account of what it means to say that a program satisfies a specification (this amounts to a semantics of the programming language, an account of the meaning of programs). None the less, Formal Methods are now routinely practised by a number of software producers.

The aim of this book is to present informal formal methods, showing the benefits of the approach even without strict formality although we use logic as a notation for the specifications, we rely on informal semantics -- a programmer's ordinary intuitions about what small, linear stretches of code actually do -- and we use proofs to the level of rigour of ordinary mathematics.

This can, of course, serve as a first introduction to strict Formal Methods, but it should really be seen much more broadly. The benefits of Formal Methods do not accrue just from the formality. The very effort of writing a specification prior to the coding focuses attention on what the user wants to get out of the program, as opposed to what the computer has to do, and the satisfaction proof, even if informal, expresses our idea of how the algorithm works. This does not require support tools, and the method -- which amounts really to methodical commenting -- is practicable in all programming tasks.

Book Structures:

The book is divided into two complementary parts, the first on Programming and the second on Logic. Though they are both about logical reasoning, the first half concerns the ideas about programs that the reasoning is intended to capture, while the second half is more about the formal machinery. The distinction is somewhat analogous to that often seen in books about programming languages a first part is an introduction to programming using the language, and a second part is a formal report on it.

To read the book from scratch, one would most likely read the two parts in parallel, and this is in fact how the material was used for the computer science course at Imperial College. However, the division into two reasonably disjoint parts means that people who already have some background in logic can see the programming story told without interruption.

Can we ever be sure that our computer programs will work reliably? One approach to this problem is to attempt a mathematical proof of reliability, and this has led to the idea of Formal Methods: if you have a formal, logical specification of the properties meant by 'working reliably', then perhaps you can give a formal mathematical proof that the program (presented as a formal text) satisfies them.

Of course, this is by no means trivial. Before we can even get started on a formal proof we must turn the informal ideas intended by 'working reliably' into a formal specification, and we also need a formal account of what it means to say that a program satisfies a specification (this amounts to a semantics of the programming language, an account of the meaning of programs). None the less, Formal Methods are now routinely practised by a number of software producers.

The aim of this book is to present informal formal methods, showing the benefits of the approach even without strict formality although we use logic as a notation for the specifications, we rely on informal semantics -- a programmer's ordinary intuitions about what small, linear stretches of code actually do -- and we use proofs to the level of rigour of ordinary mathematics.

This can, of course, serve as a first introduction to strict Formal Methods, but it should really be seen much more broadly. The benefits of Formal Methods do not accrue just from the formality. The very effort of writing a specification prior to the coding focuses attention on what the user wants to get out of the program, as opposed to what the computer has to do, and the satisfaction proof, even if informal, expresses our idea of how the algorithm works. This does not require support tools, and the method -- which amounts really to methodical commenting -- is practicable in all programming tasks.

Book Structures:

The book is divided into two complementary parts, the first on Programming and the second on Logic. Though they are both about logical reasoning, the first half concerns the ideas about programs that the reasoning is intended to capture, while the second half is more about the formal machinery. The distinction is somewhat analogous to that often seen in books about programming languages a first part is an introduction to programming using the language, and a second part is a formal report on it.

To read the book from scratch, one would most likely read the two parts in parallel, and this is in fact how the material was used for the computer science course at Imperial College. However, the division into two reasonably disjoint parts means that people who already have some background in logic can see the programming story told without interruption.

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.

No information is available for this author.

Book Categories

Computer Science
15
Introduction to Computer Science
32
Introduction to Computer Programming
52
Algorithms and Data Structures
24
Artificial Intelligence
24
Computer Vision
28
Machine Learning
6
Neural Networks
22
Game Development and Multimedia
25
Data Communication and Networks
5
Coding Theory
14
Computer Security
8
Information Security
34
Cryptography
3
Information Theory
17
Computer Organization and Architecture
22
Operating Systems
1
Image Processing
10
Parallel Computing
4
Concurrent Programming
20
Relational Database
3
Document-oriented Database
13
Data Mining
16
Big Data
17
Data Science
23
Digital Libraries
22
Compiler Design and Construction
26
Functional Programming
11
Logic Programming
26
Object Oriented Programming
21
Formal Methods
69
Software Engineering
3
Agile Software Development
7
Information Systems
5
Geographic Information System (GIS)

Mathematics
66
Mathematics
13
Algebra
1
Abstract Algebra
27
Linear Algebra
3
Number Theory
8
Numerical Methods
2
Precalculus
10
Calculus
1
Differential Equations
5
Category Theory
10
Proofs
19
Discrete Mathematics
24
Theory of Computation
14
Graph Theory
1
Real Analysis
1
Complex Analysis
14
Probability
43
Statistics
7
Game Theory
5
Queueing Theory
13
Operations Research
16
Computer Aided Mathematics

Supporting Fields
19
Web Design and Development
1
Mobile App Design and Development
28
System Administration
2
Cloud Computing
9
Electric Circuits
6
Embedded System
26
Signal Processing
4
Network Science
3
Project Management

Operating System
Programming/Scripting
6
Ada
13
Assembly
34
C / C++
8
Common Lisp
2
Forth
35
Java
12
JavaScript
1
Lua
15
Microsoft .NET
1
Rexx
12
Perl
6
PHP
66
Python
12
R
1
Rebol
13
Ruby
2
Scheme
3
Tcl/Tk

Miscellaneous