Abigail wrote:
Hi,
I have been searching papers about tha raltionship
between formal methods in software engineering and
functinal programmming, but i haven't found enough
information.
Functional programming in pure functional languages like Haskell can
help to make programs easier to reason about - but it doesn't _remove_
the need for formal methods.
For example, there are laws about certain classes such as Monad and
Monoid which all instances of those classes must follow in order to be
considered "proper" Monads or Monoids. However, in order to reason about
functions defined over all Monads (say), we need to know that those laws
hold for _all_ possible Monads (without laws, we don't really know
anything about the methods of Monad - in a non-strict language, the
methods might not even be well-defined for certain inputs). But Haskell
doesn't even have a way to _state_ these laws formally, much less
_prove_ them!
I am working on a functional programming and specification language in
my spare time which does have such formal methods features built-in, but
it is not even implemented yet. (I can email you if I ever write a paper
on it, but it may be some years before that happens.)
However, there are various other angles which you can research:
1. Proofs as programs: _Constructive_ proofs of theorems can be
automatically converted into programs in a functional programming
language - although these programs are not always efficient. Indeed it
is possible that a generated program will be far too inefficient to be
useful. See for example "Proofs, Programs and Executable Specifications
in Higher Order Logic", a Phd thesis by S Berghofer at
http://www4.in.tum.de/~berghofe/papers/phd.pdf
1a. Models as functional programs: The very first sentence in Chapter 1
of the thesis I just cited, says: "Interactive theorem provers are tools
which allow [one] to build abstract system models, often in some kind of
functional programming language involving datatypes and recursive
functions."
2. Dependent types: By programming in a dependently-typed functional
programming language such as the research language Epigram, it is
possible to write functional programs whose types force them to be
correct. See for example "Why Dependent Types Matter" by Thorsten
Altenkirch, Conor McBride, and James McKinna. However, in my opinion
this is only useful for simple "sized types" such as "a list of length
6". For more complicated properties, I believe this approach is
unnecessarily difficult, and does not match how mathematicians or
programmers actually work. My approach (see above) clearly separates the
programming, the theorems and the proofs, and (in principle) allows all
three to be written in a fairly "natural" style. As opposed to dependent
types which, in Epigram at least, seem to require threading proofs
through programs (for some non-trivial proofs).
3. Separate formal methods tools for Haskell: My approach is to
integrate formal methods directly into the essential core of a language,
but this is quite unusual to say the least - a more normal thing to do
(whether for functional or imperative languages) is prepare a separate
formal methods tool for an existing programming language. This has been
done for Haskell - see "Verifying haskell programs using constructive
type theory" by Abel et. al. at
http://portal.acm.org/citation.cfm?id=1088348.1088355
I have not considered testing in this email because another email
already mentioned QuickCheck.
--
Robin
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
