ABEL(ID:1780/abe001)OO Language with specification semanticsfor Abstraction Building Experimental Language follow up to the abstraction work in the Simulas, ended up with somewhat functional nature. Strongly-typed object-oriented language with contravariant semantics. Inherited interfaces are not required to be subtypes Places People: Structures: Related languages
References: Introduction ABEL is a language together with a formal logic for use in program development. The overall goal has been to support specification and program development through semi mechanical aids for reasoning and verification. It has been of major concern that the language and the associated reasoning formalism are such that consistency requirements and other proof obligations are as simple and manageable as possible. In particular we have sought to: - offer language constructs well suited for mechanical aids to reasoning, with some emphasis on mechanisms for constructive specification, - encourage modularization and abstract specification of interfaces, - facilitate reusability of modules through the use of parameters, - offer powerful ways of putting modules together, including inheritance, restriction, inclusion, extension, as well as assumption specification and checking, and - enable simple and manageable proof obligations, including those related to the composition and (internal) consistency of modules, in the form of first order formulas. A major idea behind ABEL has been to allow the same language cover all stages of program development from abstract requirement specifications to efficient low level programming. Thus ABEL includes facilities for non constructive requirements specification, constructive specification, applicative programming, and object oriented, imperative programming. (We let the term "specification" cover all of these.) We have tried to build the language around a few concepts which may be applied at all levels. Different stages may be related to each other through a concept of module simulation. If a low level module is proved to simulate an abstract one, then the latter may be used as an abstract specification of the low level module. In the sequel we emphasize an applicative language level called TGI, which stands for terminating generator induction. TGI specifications give rise to convergent rewrite rules, which enable efficient manipulation of formulas and other expressions for purposes of simplification and proof. At the TGI level all proof obligations in connection with the composition of modules and module simulation are quantifier free formulas in constructively defined functions, provided that user specified axioms are quantifier free. ABEL includes logic for partial functions, also at the TGI level. The ABEL language has been developed at the University of Oslo over a period of more than 15 years, mainly by the authors, and in close interaction with a regular student course on program specification and verification. The most important sources of ideas have been as follows: SIMULA 67 (classes and subclasses), the LARCH activity (generator induction), and OBJ (order sorted algebras). 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: ABEL ABEL ABEL is a language together with a formal logic for use in program development. The overall goal has been to support specification and program development through semi-mechanical aids for reasoning and verification. Major concerns for the language and the associated reasoning formalism are that consistency requirements and other proof obligations are as simple and manageable as possible. In particular it was sought to offer language constructs well suited for mechanical aids to reasoning, with some emphasis on mechanisms for constructive specification; to encourage modularization and abstract specification of interfaces; to facilitate reusability of modules through the use of parameters; to offer powerful ways of putting modules together, including inheritance, restriction, inclusion, extension, as well as assumption specification and checking; and to enable simple and manageable proof obligations, including those related to the composition and (internal) consistency of modules, in the form of first order formulas. A major idea behind ABEL has been to allow the same language cover all stages of program development from abstract requirement specifications to efficient low level programming. Thus ABEL includes facilities for non-constructive requirements specification, constructive specification, applicative programming, and object oriented, imperative programming. (The term "specification" covers all of these.) The language is built around a few concepts which may be applied at all levels. Different stages may be related to each other through a concept of module simulation. If a low level module is proved to simulate an abstract one, then the latter may be used as an abstract specification of the low level module. The ABEL language has been developed in close interaction with a regular student course on program specification and verification. The most important sources of ideas have been SIMULA 67, LARCH, and OBJ. 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. Extract: ABEL ABEL has been developed at Oslo University. Distinctive features are: ? Parameterized types and subtypes (syntactic and semantic), also object oriented classes. ? Modules parameterized explicitly by types and implicitly by loose functions (renameable). ? Loose specifications by first order axioms. ? Constructive specifications are based on generator inductive definitions of types and functions. Definition of existing loose functions trigger proof obligations. ? Function definitions by terminating generator induction, TGI, give rise to convergent rewrite rules and to covariant profile families based on syntactic subtypes, syntactic totality checks, as well as mechanically defined well-definedness conditions. ? Extension to higher order types and functions is planned. Extract: Reusability 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]. Introduction Specifications are used to express system requirements and system design at different levels of abstraction. Ultimately specifications will function as correctness criteria for the implemented system. Formal techniques, expressing system properties by axioms, say in a typed first order formula language, may allow mechanized aids to reasoning about the specifications themselves, as well as aids to program development and verification with respect to the specifications. Specifications should be easy to understand, analyze, and to experiment with. Good modularization is essential for more detailed system specification and implementation. Even so, using free axiomatic techniques may lead to specifications which are internally inconsistent and therefore useless. Consistency proofs are difficult in general, so there is a need for linguistic aids for avoiding inconsistencies, or at least detecting inconsistency at an early stage. We believe that constructive specifications represent important intermediate stages between property oriented specifications and implementation, for the following reasons: (1) It is possible to provide better syntactic control with consistency (as well as completeness). (2) Verifying that all property requirements are fulfilled by a constructive specification is a way of proving the consistency of the former. (3) A constructive specification is an "abstract", but executable, program which may function as a prototype system (possibly inefficient). It is clear that requirements specifications will normally be expressed by means of free axioms. However, if some of the types and functions involved are constructive, then the axioms may well be easier to understand, and more efficient and powerful mechanized tools for reasoning about the specifications are likely to be available. An example is the requirement specification in [5] of a many-lift system whose internal consistency is almost trivial. We shall show how subtypes may be used to enhance expressiveness and strengthen syntactic controls in the context of a certain style of constructive specification. More specifically subtyping is a means to: - make expression typing stronger and more flexible, - aid in the use of partial functions, - introduce natural function overloading for taking advantage of special cases, - aid in defining types not freely generated, - express representation invariants in data structures, and - introduce implementation related capacity constraints. Although the results of this paper to a large extent are language independent, we need a language in which to express our ideas. For that purpose we use the applicative core of a specification and programming language called ABEL, (Abstraction Building, Experimental Language), developed at the University of Oslo, and based on a typed logic for partial functions. A separate paper, will discuss the extension to higher order. The most important sources of ideas have been as follows: SIMULA 67 (classes and subclasses), the LARCH and IOTA activities (generator induction), and OBJ (order sorted algebras). The so called TGI fragment of ABEL deals with constructively defined types and functions (both partial and total). TGI stands for "Terminating Generator Induction". TGI specifications give rise to convergent sets of rewrite rules, which enable efficient manipulation of expressions for purposes of simplification and proof. Two species of subtypes are considered: syntactic subtypes defined inductively, and semantic subtypes defined by means of predicates. A concept of convex subtype is identified, useful for the strengthening of expression typing. An important property of the TGI fragment is that all consistency related proof obligations can be identified and formulated mechanically (as formulas in typed first order logic). We also believe that the syntactic TGI restrictions will provide useful guidance for programmers who are not trained algebraists. The use of syntactic TGI-like restrictions have also been advocated by Turner for educational purposes. |