Up Next
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:

  1. 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.
  2. 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.
  3. 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).
  4. 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 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

Up Next