Go up to Top
Go forward to 2 Partial recursive functions through free extensions
1 Introduction
The ultimate goal of software development using
algebraic specifications is to get a program that meets a
formal specification. By showing that a program meets
a given specification, as a side-effect the specification
is proven to be consistent.
No formal relation of CASL to existing
programming languages has been worked out yet.
In the literature, there are three approaches:
- Restrict the expressibility of the specification language in such a way
that it becomes executable. This approach was taken by OBJ3.
The main argument against this approach is that
it mixes up specification and programming: while specifications
should be clear and easy to understand, programs should
be efficient. Practice shows that you can hardly have both.
Thus executable specification languages lead to a lack of
clarity due to lack of expressiveness.
- Build a specification language over a programming
language. The prominent example here is Extended ML,
which is built over Standard ML. The main critical
point seems here to be the immense complexity
of the (semantics of the) language.
- Semantically link a specification and a programming language,
for example by extracting
an algebra from the denotation of a program
in order to be able to define what it means
that a program meets a specification.
With this semantical basis, one can
then prove that a program meets a specification.
Larch has (apart from the Larch shared language
that is comparable to CASL) explicit interface languages to different
programming languages that allow to fiddle with the
not-so algebraic details of programming languages (like exceptions
and procedures) and to describe
how algebras are extracted form programs (two-tiered approach).
- Semantically link a specification and a programming language
and define transformations from
the specification to the programming language
(and, of course, transformations within both languages).
Software development then becomes application of transformation.
In this note, we identify sublanguages of CASL in which
can serve as domains of transformations
to functional programming languages.
Each specification in these sublanguages
- has a unique model (up to isomorphism), and
- can easily be realised by a (functional) program.
These design specifications can be considered to be
abstract "programs". Of course,
this approach is not intended to replace the
formal bridge from CASL to programming languages:
Only some very limited aspects of functional programming
languages can be covered. In general, one wants to
write functional programs using also more sophisticated
aspects of functional programming languages.
But the advantage of this approach
is that these "programs" are independent of any
particular programming language.
CoFI
Note: L-9 --Version 1.0-- 21 March 1998.
Comments to till@informatik.uni-bremen.de