Home > Archive > Functional > June 2007 > Spec langs (e.g. Z) for FP?
You are viewing an archived Text-only version of the thread.
To view this thread in it's original format and/or if you want to reply to
this thread please [click here]
| Author |
Spec langs (e.g. Z) for FP?
|
|
| raould@gmail.com 2007-06-04, 7:05 pm |
| hi,
I know you can e.g. use Coq and spit out O'Caml. But can you apply
e.g. Z to Haskell (apparently yes e.g.: http://citeseer.ist.psu.edu/266634.html),
O'Caml, Scheme, Erlang, etc? In general, do FPs have modeling
languages for them along the lines of Eiffel's DbC or Java's JML or
Ada's Praxis stuff? Or, perhaps in other words, what are the concrete
ways people do DbC / "correct by construction" in FP?
Thanks for any references!
[I have been / am looking via Google etc. but find that searching for
"functional" and "specification" tends to not give me specs for FP but
functional specs for e.g. imperative/oopies.]
sincerely.
| |
| dbenson@eecs.wsu.edu 2007-06-04, 7:05 pm |
| > "correct by construction" in FP?
I program almost exclusively in SML/NJ. First I write the signature
for a structure(module). Then, once in a while, I use comments to add
pre- and post- conditions. However, usually the signature makes these
conditions obvious.
There are formal development techniques for writing the actual
functions, but ordinarily everything I write is already divided into
such small functions that I can just do it in my head, rather than go
through the formalities.
The biggest win, IMO, is the type checking. This catches most errors
at compile time, although some debugging often remains. The second
biggest win is functional style, whenever possible, leaving imperative
programming to blast my way out of an early design error. I do this
when I'm rushed and always hope to go back to do the redesign. (Maybe
I actually have done this a couple of times.)
I write concurrent code, using eXene as my GUI. For this form of
coding, I know of no useable, implemented development tools. Its not a
problem as I am the only programmer...
| |
| Dirk Thierbach 2007-06-05, 4:05 am |
| raould@gmail.com wrote:
> Or, perhaps in other words, what are the concrete
> ways people do DbC / "correct by construction" in FP?
In Haskell, one way to that is to use the type system to encode some
of the simpler requirements, and Haskell itself as a specification
language to encode the more complex ones. One can then either test the
specification directly for some values (which corresponds to agile
"unit tests"), use QuickCheck to test them for a number of randomly
generated example values, or one can prove the specification by hand,
where often enough equational reasoning and induction on algebraic
datatypes is sufficient.
The specifications expressed by the type system are of cause
automatically "proved" by the Compiler.
Specifications usually go beyond DbC and can really encode the complete
desired behaviour. As long as the code is functionally pure, this is
actually a lot easier than in imperative languages.
> [I have been / am looking via Google etc. but find that searching for
> "functional" and "specification" tends to not give me specs for FP but
> functional specs for e.g. imperative/oopies.]
Googling for "Haskell" and "QuickCheck" should turn up some examples.
- Dirk
| |
| Jose Juan Mendoza Rodriguez 2007-06-07, 10:06 pm |
|
Hi,
you might want to check the following papers,
* Program Specification and Data Refinement in Type Theory
Zhaohui Luo
LFCS report ECS-LFCS-91-131
* Deliverables: a categorical approach to program development in
type theory
Rod Burstall and James McKinna
LFCS report ECS-LFCS-92-242
* Typing Abstract Data Types
Judith Underwood
LFCS report ECS-LFCS-95-320
all of them available from
http://www.lfcs.informatics.ed.ac.uk
Quoting from ECS-LFCS-92-242:
"The motivation for such a definition goes right back to Hoare's
original paper on axiomatic semantics [14], and, like the logic of
triples which bears his name, expresses in a formal system the
informal notion of a program, together with a certificate of some
specified input/output behaviour."
Kind regards.
--
Jose Juan Mendoza Rodriguez
let me=josejuanmr in
let privacy=iespana in
let net=es in
me@privacy.net
| |
|
|
|
|
|