Functional - most usable formal methods?

Author

most usable formal methods?

raould@gmail.com

2007-04-12, 10:03 pm

hi,

This will be a nebulous question, I already know...

After reading Dijkstra's "On the cruelty of really teaching computing
science"

http://www.cs.utexas.edu/users/EWD/...xx/EWD1036.html

I wonder what is the fn language with the most light-weight formal
methods available? I'm trying to find something that isn't "go program
in Coq" but isn't "just hack things up in an un/dynamically-typed
language and who cares about runtime crashes!". I would hazard to
guess that there's stuff for O'Caml? Any personal experiences to
relate? Preferences? Warnings?

[I did Z back during my abortive Master's. I've read up on JML,
Eiffel, Sather, Praxis Ada, etc. I've probably proved things about my
programs when in college... But I really haven't used formal methods
of any sort in entirely too long. I'm scared to have to spend a lot of
time re-educating myself. I guess I'm being a bad example a la
Dijkstra's screed in that I want to be able to just hack up my code
yet somehow get the advantages of more formalization. With Java I
could at least use static checkers like the gloriously awesome
FindBugs, so maybe I should just stick with that?]

thanks for any input.

dbenson@eecs.wsu.edu

2007-04-12, 10:03 pm

> guess that there's stuff for O'Caml?

I use Standard ML almost exclusively, using the SML/NJ compiler. I
find that for the vast majority of programming, ordinary reasoning
plus the type inference and checking in SML suffices to rapidly
produce correct code which even using SML/NJ runs adequately fast.

So I don't use, in detail, what are called formal methods. Your milage
may vary...

Dirk Thierbach

2007-04-13, 4:04 am

raould@gmail.com wrote:
> This will be a nebulous question, I already know...

> I wonder what is the fn language with the most light-weight formal
> methods available? I'm trying to find something that isn't "go program
> in Coq" but isn't "just hack things up in an un/dynamically-typed
> language and who cares about runtime crashes!".

Nebulous answer: It's often a lot easier to use formal methods in
the absence of side effects, so try to stay as pure as possible
when programming. You can use a good type system to encode at least
some requirements. Haskell QuickCheck can also be a nice replacement
for a theorem prover (and once you get your program to work, nobody
stops you from proving the predicates manually, if you don't trust the
testing enough).

-Dirk

Phil Armstrong

2007-04-13, 7:04 pm

Dirk Thierbach <dthierbach@usenet.arcornews.de> wrote:
> raould@gmail.com wrote:
>
>
> Nebulous answer: It's often a lot easier to use formal methods in
> the absence of side effects, so try to stay as pure as possible
> when programming. You can use a good type system to encode at least
> some requirements. Haskell QuickCheck can also be a nice replacement
> for a theorem prover (and once you get your program to work, nobody
> stops you from proving the predicates manually, if you don't trust the
> testing enough).

This livejournal exchange seems apropos this point:

http://totherme.livejournal.com/3674.html

Or to paraphrase, you can use a combination of specifications written
in QuickCheck and specifications written via the Haskell type sytem to
iteratively resolve your code from two directions. Hopefully when the
two 'meet in the middle' the code becomes obvious...

Phil

--
http://www.kantaka.co.uk/ .oOo. public key: http://www.kantaka.co.uk/gpg.txt

raould@gmail.com

2007-04-13, 7:04 pm

thanks to all for the comments and suggestions.

I've used SML and did find that it would help me write more "correct"
programs, although I've read that other people don't always have that
experience (http://totherme.livejournal.com/3674.html). I've also read
about QuickCheck, I'll go follow that live journal discussion Phil
mentioned.

sincerely.

Albert Y. C. Lai

2007-04-13, 10:02 pm

Dirk Thierbach wrote:
> Haskell QuickCheck can also be a nice replacement
> for a theorem prover

QuickCheck and similar things (e.g., SmallCheck) certainly qualify as
lightweight formal methods. The important point is writing
specifications (can be incomplete) in a language with both a formal
grammar and a formal semantics. The machine check can be partial because
we settle for lightweight. To wit, Alloy (http://alloy.mit.edu/) takes
first-order logic and checks only bounded-size universes; ESC/Java
(http://research.compaq.com/SRC/esc/) takes imperative programming and
assertions and checks only the first iteration whenever it encounters a
loop. These are considered acceptable as lightweight formal methods.
There is similarly no sin in QuickCheck checking a few random cases.

Ulf Wiger

2007-04-16, 4:05 am

>>>>> "A" == Albert Y C Lai <trebla@vex.net> writes:

A> Dirk Thierbach wrote:[color=darkred]

A> QuickCheck and similar things (e.g., SmallCheck) certainly
A> qualify as lightweight formal methods. The important point is
A> writing specifications (can be incomplete) in a language with
A> both a formal grammar and a formal semantics.

I just thought I'd point out that there is a commercial version
of QuickCheck (written in Erlang), which has some powerful
features not found in the Haskell QuickCheck. One of the
very useful additions is stateful testing; another is
and advanced form of "shrinking"*. A paper was written
about this for the 2006 SIGPLAN Erlang Workshop.
(Here's a link to the powerpoint slides:
http://www.erlang.se/workshop/2006/Hughes.ppt )

* Automatically searching for the smallest counter-example.

(To be clear, I have no commercial stake in the product, but
can happily say that we've started using it in our development
projects, and have already started seeing some results that
would hardly have been possible without QuickCheck.)

BR,
Ulf W
--
Ulf Wiger, Senior Specialist,
/ / / Architecture & Design of Carrier-Class Software
/ / / Team Leader, Software Characteristics
/ / / Ericsson AB, IMS Gateways

Freppa

2007-04-19, 1:56 am

http://Pamela-Anderson-in-nylons.in...hp?movie=148803

Sponsored Links