What is a Formal Method ?
In Computing Science,
and in Hardware and Software Engineering !
Dines Bjørner
CSE: Computer Science and Engineering
IMM: Informatics and Mathematical Modelling
Building 322, Richard Petersens Plads
DTU: Technical University of Denmark
DK-2800 Kgs.Lyngby, Denmark
E-Mail: db@imm.dtu.dk, URL: www.imm.dtu.dk/ db
October 12, 2003
-
Abstract:
- An attempt is made to encircle the concept of `Formal Method' as it
has become known in Computing.
We put forward our own view of this.
We discuss, briefly, whether the term `formal method' is an
appropriate term -
in the contexts in which it is being commonly used.
- To balance our views off, we bring references to other `Formal Method'
delineating statements.
- This web page is part of a series of web pages resulting from the
EU/IST CoLogNETetwork of
Excellence
project.
See further
URL references at the bottom of this page.
Some definitions:
-
What is a Method ?
- By a method is meant a set of
principles
that are used in
selecting and applying a number of
techniques
and
tools
in order to
identify and analyse a problem and
synthesize (construct) a solution to the problem.
- Normally one would expect a good method to be ``efficient'' and
result in ``efficient'' solutions.
-
What is meant by Formal ?
In the context of software (hardware) development, the term `Formal'
is usually considered to imply the following:
- There is a
language,
a so-called
formal
language,
for expressing problem characterisations and/or
problem solutions, at various levels of abstraction.
- We usually refer - interchangeably -
to such a language as a specification, a design, or a
programming language.
- That language must have the following three properties in order to
qualify as a formal specification (design or programming) language:
- It must have a precise, ie., a mathematically well defined
syntax
- something which defines all such
sentences and/or
diagrams (or other) which are members of the language.
- It must have a precise, ie., a mathematically well defined
semantics
- something which to every
syntactically well-formed
sentence and/or diagrams (or other) which are members of the
language ascribe a precise meaning in terms of some mathematical
structure.
- It must have a
proof system:
That is,
a set of axioms and
inference (ie., deduction) rules by means of which one can reason over
all syntactically well-formed sentence and/or diagrams (or other)
of the language.
- It is expected that the Language Semantics have been shown to be
a model of the Proof System.
-
What, then, is a Formal Method ?
A `Formal Method', then, is a `Method' some of whose main `Techniques' and
main `Tools' depend crucially upon the use of Formal Languages.
-
Some Observations:
- A major Tool, in development (ie., in analysing problems and in
synthesising problem solutions), is that of language.
- Major Techniques, in development, are then various calculi that
apply to fragments or whole specifications and yield sentences in
some formal language.
- Derivative Tools then support the use of languages and calculi.
-
Whither Formal Method ? -- Why not just Formal
Techniques ?
- Now, since a `Method' is taken to be used by humans, and since we take
it, as a dogma, that the selection and application of method principles
is to be decided upon by these humans, from case to case, as inspired
by the complexities and/or novelties (or familiarities) of the
problem, we conclude that a method cannot be formal !
- Instead we resolve that some method Techniques and some method
Tools (to support, or express) these Techniques, can, indeed, be
formal, respectively be based on formal languages.
Other views of what `Formal Methods' are:
On linguistics notions
- from The Collins
English Dictionary © 2000 HarperCollins Publishers:
-
Language:
The scientific study of language.
-
Semiotics:
The study of signs and
symbols, esp. the
relations between written or spoken signs and their referents in the
physical world or the world of ideas.
-
Syntactics:
The branch of semiotics
that deals with the formal
properties of symbol systems; proof theory.
-
Pragmatics:
- The study of those aspects of language that cannot be considered
in isolation from its use,
- the study of the relation between symbols and those who use them.
-
Syntax:
- the branch of linguistics that deals with the grammatical
arrangement of words and morphemes in the sentences of a language or
of languages in general,
- the totality of facts about the grammatical arrangement of words
in a language,
- a systematic statement of the rules governing the grammatical
arrangement of words, diagrammatic symbols, and morphemes
in a language,
- (Logic) a systematic statement of the rules governing the
properly formed formulas of a logical system,
- any orderly arrangement or system.
-
Semantics:
- The branch of linguistics that deals with the study of meaning,
changes in meaning, and the principles that govern the relationship
between sentences or words and their meanings,
- the study of the relationships between signs and symbols and
what they represent,
- (Logic)
- the study of interpretations of a formal theory,
- the study of the relationship between the structure of a theory
and its subject matter,
- (of a formal theory) the principles that determine the truth or
falsehood of sentences within the theory, and the references of its
terms.
-
Proofs, Proof Theory, and Proof Systems:
-
Proof:
- (General) any evidence that establishes or helps to establish the truth,
validity, quality, etc., of something,
- (Maths, logic) a sequence of steps or statements that
establishes the truth of a proposition.
-
Proof Theory:
the branch of logic that
studies the syntactic properties of
formal theories, esp. the syntactic characterization of deductive
validity.
-
Proof System:
a set of axioms and
induction rules for
carrying out profs.
-
Models and Model Theory:
-
Model:
- an interpretation of a formal system under which the theorems
derivable in that system are mapped onto truths,
- a theory in which a given sentence is true.
-
Model Theory:
The branch of logic that
deals with the properties of models;
the semantic study of formal systems.
See other `Formal Methods' pages:
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
What is a Formal Method ?
In Computing Science,
and in Hardware and Software Engineering !
This document was generated using the
LaTeX2HTML translator Version 2K.1beta (1.47)
Copyright © 1993, 1994, 1995, 1996,
Nikos Drakos,
Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999,
Ross Moore,
Mathematics Department, Macquarie University, Sydney.
The command line arguments were:
latex2html -split 0 -toc_depth 6 what
The translation was initiated by on 2003-10-12
2003-10-12