20-04-2012, 02:47 PM
Functional programming languages for verification tools: a comparison
of Standard ML and Haskell
Functional Programming For verification tools.pdf (Size: 194.68 KB / Downloads: 42)
Introduction
Concurrent software and hardware systems play an in-
creasing role in today's applications. Due to the large
number of states and to the high degree of non-determin-
ism arising from the dynamic behaviour of such systems,
testing is generally not su±cient to ensure the correct-
ness of their implementation. Formal speci¯cation and
veri¯cation methods are therefore becoming more and
more popular, aiming to give rigorous support for the
system design and for establishing its correctness prop-
erties, respectively (cf. [1] for an overview).
Verification tools
The domain on which we compare SML and Haskell
is that of veri¯cation tools. The term \veri¯cation tool"
covers any tool whose task it is to assist in checking the
correctness of some artefact. Usually the artefact con-
cerned is (an abstraction of) something produced in the
software or hardware development process.
We introduce Truth and the CWB and brie°y sum-
marise their histories before discussing the characteristic
features of veri¯cation tools in general.
The Edinburgh Concurrency Work-bench, in SML
Work on the CWB3 began in 1986. The CWB's key
strength is its breadth: a variety of di®erent veri¯cation
methods are supported for several di®erent process alge-
bras. In particular, it allows users to:
The verification platform Truth, inHaskell
In terms of features, Truth5 is similar to the CWB.
In its current version, it supports tableau-based model
checking for the full ¹-calculus and game-based model
checking for the alternation-free subcalculus. Both op-
erate on ¯nite transition systems, given in terms of CCS
processes. The latter can be visualised and simulated
in an interactive fashion, to help the user understand
Truth's answers. Current development activities con-
centrate on the parallel implementation of model check-
ing on a cluster of workstations and on a speci¯cation
language compiler generator which, given the de¯nition
of a language, automatically generates a corresponding
parser and a semantic evaluator.
The space of programming lan-guages
Clearly Haskell and SML, the languages of Truth
and the CWB, have a great deal in common: both are
basically functional languages and both have static type
systems which are strong in the sense that a well-typed
program will be free of certain classes of runtime errors.
Moreover, both are minority languages, with their origins
in academia. What is the signi¯cance of these features
for veri¯cation tools?
Considerations for future projects
There have been positive and negative aspects to both
our sets of experiences with Haskell and SML, as there
would doubtless have been with whatever language we
had chosen. Overall, we consider Standard ML to be
a slightly better choice for our kind of application than
Haskell, more because of a more stable environment
of supporting tools than because of language features.
Of course, there are many alternatives including other
functional languages with which we have less experience;
O'Caml might be a strong candidate.