What is meant by
"A Formal Technique cum Method"?
- 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.
- We also refer, here, to a "subjective", ie., not necessarily
complete, List of Some Formal
Techniques cum Methods.
-
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 proof
(ie., inference and/or 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:
|
