Algebraic functional language 

Technical University of Berlin.

Algebraic programming language which integrates both concepts of algebraic specification and functional programming. Strongly-typed, higher-order, strict applicative language, with algebraic specification. Uses parameterized structures rather than polymorphism.

Opal is a strongly typed, higher-order, strict, pure functional language, and as such can be classified alongside ML, Haskell, and other modern functional programming languages. However, the language also has a distinctive algebraic flavour in the tradition of languages such as CIP-L, Obj, and others.

The language includes what we consider to be mandatory for research and teaching on:

  • optimizing compilation of algebraic languages

  • formal programming methodology

  • methodology of implementing large software systems

The following characteristics give an overview of the language design:

  • Modularization by means of separated signature and implementation parts of structures .

  • Selective imports of items from structures.

  • Parameterized structure, with support to shortcut the notation of actualization morphisms, or to let them be inferred by the compiler.

  • Free constructor views on sorts, which allow pattern-based function definitions in spite of quite different implementations.

  • Unrestricted overloading of names, considering complex contexts for the overloading resolution.

  • Puristic scheme language with no built-in data types (except of booleans and denotations).

Opal-1 and its predecessor Opal-0 have been used for some time at the Technical University of Berlin in basic and advanced computer science courses, as well as in several research projects. Opal has been used to implement its own compiler.

Related languages
OPAL => OPAL-0   Implementation
OPAL => OPAL2   Successor

  • Didrich, Klaus; Fett, Andreas; Gerke, Carola; Grieskamp, Wolfgang; Pepper, Peter "OPAL: design and implementation of an algebraic programming language" pp228-244 view details
          in Proceedings of the international conference on Programming languages and system architectures, April 1994, Zurich, Switzerland view details
  • Cerioli, Maura; Gogolla, Martin; Kirchner, Helene; Bruckner, Bernd Krieg; Qian, Zhenyu; Wolf, Markus "Algebraic System Specification and Development - Survey and Annotated Bibliography" Second Edition Compass Group Bremen 1997 view details Abstract: Methods for the algebraic specification of abstract data types were proposed in the early seventies in the USA and Canada and became a major research issue in Europe shortly afterwards. Since then the algebraic approach has come to play a central role in research on formal program specification and development, as its range of applications was extended to the specification of complete software systems, to the formal description of the program development process, and to the uniform definition of syntax and semantics of programming languages. Today this approach extends beyond just software to the development of integrated hardware and software systems. These flourishing activities in the area of algebraic specifications have led to an abundance of approaches, theories and concepts, which have universal algebra, category theory and logic as a common mathematical basis.
    The present volume is an annotated bibliography which attempts to provide an up-to-date overview of past and present work on algebraic specification. No attempt is made to provide a coherent introduction to the topic for beginners the intention is rather to provide a guide to the current literature for researchers in algebraic specification and neighbouring fields. Some indications of how the different approaches are related are included. ps Extract: The Opal Compilation System
    The Opal Compilation System
    OPAL is an algebraic high-level language[...]. An important aspect of the work performed on the development of the algebraic programming language OPAL is to provide tools for development of adequate software in an algebraic framework. Therefore the OPAL COMPILATION SYSTEM OCS has been developed which supports the development of modular software systems. The kernel of OCS is an optimizing compiler that generates efficient code for OPAL-programs. The current version of the OPAL COMPILATION SYSTEM is OCS 2.1e which has been released in July 1995.
    Apart from the kernel, the OPAL compilation system contains a restructured and augmented standard library, a revised scheme for incorporating C code, and a introductory tutorial [338]. A documentation system for OPAL was developed, which supports a literate programming style which can also deal with code which is not or only partially documented.
    Extract: OPAL
    OPAL. The development of the Algebraic Programming Language OPAL is an ongoing activity at TU Berlin. The aim of this work is to provide an algebraic high-level language which is equipped by a compilation system for generating efficient code. The Algebraic Programming Language OPAL (with initial emphasis on functional programming) has been extended by a property language, so every part of a software development from the requirements specification to the final implementation can now be expressed within OPAL. We hope for an even better integration in the successor to OPAL, called OPAL2. The language design took place in 1995 and first tools are now being worked on. We plan to reuse as much of the current OPAL backend as possible, so we expect to inherit the efficiency of the OPAL compilation system for a future OPAL2 system. Extract: Extended ML
    Extended ML
    The long-term goal of work on Extended ML is to provide a practical framework for formal development of Standard ML programs together with an integrated suite of computer-based specification and development support tools and complete mathematical foundations to substantiate claims of correctness. The complete formal definition of the Extended ML language [533] constitutes an important milestone in this programme, necessary to provide a basis for further research on foundations and tools. One of the key issues that had to be resolved was the design of a logic suitable for describing properties of Standard ML programs, taking into account features like recursive type and function definitions, exceptions, polymorphism, and non-termination. A number of errors in the Standard ML semantics [679] have been discovered in the course of this work [526]. Work has begun on rules for proving theorems about EML specifications, to be used in verifying correctness conditions that arise in the course of formal development. Research has so far concentrated on equality reasoning [530] and quantifier rules.
    The length and requisite formality of the definition of Extended ML renders it rather difficult to penetrate. Accordingly, [532, 534] provides an informal overview of the definition, explaining most of the main issues involved and justifying some of the choices taken.
    The demand for reusability originates from economic considerations and attempts towards standardization. Rather than always starting from scratch, the use of existing components is cheaper and also less error-prone. A central problem for the identification and the correct use of reusable components is the abstract description of such components. A formal specification is the only form of description that can serve as a basis for a correctness proof; it can be processed automatically and it establishes a degree of confidence in the functionality of the component that is particularly important if a component has to be modified before being reused.
    Goguen [404] proposes the algebraic specification language OBJ as well-suited for the design of reusable software systems. A component's interface is specified as an abstract data type and may be parameterized by other components. Combination of components is possible by instantiation using appropriate fitting morphisms. A similar approach is used in Extended ML [836], [848].
    In ACT TWO [315] components are modules, which consist of two interface specifications, i.e. an export specification and an import specification, and a body specification which implements the export specification in terms of the import specification. Similarly, in LARCH [445], a component consists of a pair, an "abstract" interface specification and an implementation. Here the implementation is written in a conventional programming language. A similar distinction between a requirement and a design specification is made in PAnndA-S, the language of the PROSPECTRA project [138], based on the notion of visible and private interface in Ada. Ada bodies are generated semi-automatically by transformation.
    In the approach of [655] a component consists of four parts at four different levels of abstraction: a requirement specification, a design specification, a source program and object code. Components are written in a so-called wide spectrum language which provides facilities for system design and software development at many levels of abstraction. Matsumoto uses Ada, which has as a consequence that the requirement specification is merely an informal description. CIP-L [54] and COLD [341] are two languages which include algebraic specifications as well as predicative and imperative language styles in one coherent framework and therefore are better suited for such an approach.
    In the object-oriented approach of [675] a reusable component is represented by a graph of object-oriented programs, each node of which stands for one level of abstraction in the description of the software. In the approach of the ESPRIT-project DRAGON [945], a reusable component consists of a tree of algebraic specifications, where similarly to [675], each node of the tree is an instance of a certain level of an abstraction of the program with the root being the most "abstract" formal specification and the leaves representing the "concrete" implementations. A methodology for reusing components is described in [947].

          in Proceedings of the international conference on Programming languages and system architectures, April 1994, Zurich, Switzerland view details