formal methods & functional programming

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
7 messages Options
Reply | Threaded
Open this post in threaded view
|

formal methods & functional programming

abigail-7
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.
can u hel me?.
Thanks
Abigail.

__________________________________________________
Correo Yahoo!
Espacio para todos tus mensajes, antivirus y antispam ¡gratis!
Regístrate ya - http://correo.espanol.yahoo.com/ 
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: formal methods & functional programming

Jared Updike
I can't think of any Haskell papers about ``formal methods'' in
software engineering, but many papers and books talk about proving
program correctness, which is difficult in traditional, imperative
languages (which is why it is probably not stressed as much as
//testing// is in formal software methods). Paul Hudak, in the
textbook, The Haskell School of Expression
(http://www.amazon.com/gp/product/0521644089/104-7074974-5852762?v=glance&n=283155)
writes a lot about proving program correctness (especially induction
on recursive algorithms) for Haskell and purely functional programs,
reasoning mathematically.

If you want to do strenuous testing, you can use "QuickCheck:
Automatic Specification-Based Testing":
http://www.cs.chalmers.se/~rjmh/QuickCheck/

A professor I had at Caltech researches formal methods in constructing
reliable software systems, specifically using robust programming
language and compiler technology (in this case OCaml).
 http://mojave.caltech.edu/

  Jared.

On 1/14/06, Abigail <[hidden email]> 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.
> can u hel me?.
> Thanks
> Abigail.
>
> __________________________________________________
> Correo Yahoo!
> Espacio para todos tus mensajes, antivirus y antispam ¡gratis!
> Regístrate ya - http://correo.espanol.yahoo.com/
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>


--
[hidden email]
http://www.updike.org/~jared/
reverse ")-:"
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: formal methods & functional programming

Isaac Jones-2
In reply to this post by abigail-7
Abigail <[hidden email]> writes:

> 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.

I don't think there are any papers, but Galois Connections employs
Haskell and formal methods such as proof checkers in our work.  You
might email for more information:

http://www.galois.com/


peace,

  isaac
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: formal methods & functional programming

greenrd
In reply to this post by abigail-7
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: formal methods & functional programming

Lennart Augustsson
Robin Green wrote:

> 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).

I would just like to point out that there is nothing that forces you
to "thread" the proofs through the programs.  With dependent types you
have this option, but you can also write standard "Haskell" code and
have your proofs be separate.  It's up to you to choose which way you
do things.  (If you do separate proofs you can even add some construct
to the logic that makes it classical if you like.)
Furthermore, I don't see such a clear separation between your points
1 and 2.  With dependent types you are making proofs and then using them
as programs.  How much extraction you do is a matter of optimization,
I'd say.  And how efficient the extracted program is depends on which
proof you choose to do.

        -- Lennart

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: formal methods & functional programming

greenrd
Lennart Augustsson wrote:

> Robin Green wrote:
>
>> 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).
>
>
> I would just like to point out that there is nothing that forces you
> to "thread" the proofs through the programs.   With dependent types you
> have this option, but you can also write standard "Haskell" code and
> have your proofs be separate.

But wouldn't that alternate way break the principle, recommended by
Cardelli, that all code should be well-typed and the types of all terms
should be, shall we say, "plainly" deducible from the code alone (i.e.
not requiring any "difficult" reasoning on the part of the human
reader)? If not, could you give an example to illustrate your point?

>  It's up to you to choose which way you
> do things.  (If you do separate proofs you can even add some construct
> to the logic that makes it classical if you like.)
> Furthermore, I don't see such a clear separation between your points
> 1 and 2.  With dependent types you are making proofs and then using them
> as programs.  How much extraction you do is a matter of optimization,
> I'd say.  And how efficient the extracted program is depends on which
> proof you choose to do.

Well I thought someone might say something like that - which is why I
called them "angles" on the question. :)

But while statements about types and statements about values might be
inter-convertable, I think they look different and one can be more
convenient than the other for various purposes. I've only used dependent
types trivially so I could be wrong.

--
Robin
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: formal methods & functional programming

Hal Daume III-2
I confess I haven't really been following this discussion, but a friend of
mine has a recent paper that might be of interest (though it deals with ML
rather than Haskell)...

  http://math.andrej.com/2005/04/09/specifications-via-realizability/

--
 Hal Daume III                                   | [hidden email]
 "Arrest this man, he talks in maths."           | www.isi.edu/~hdaume

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe