OBJ(ID:728/obj002)Joseph Goguen 1976. A family of declarative "ultra high level" languages. Abstract types, generic modules, subsorts (subtypes with multiple inheritance), pattern-matching modulo equations, E-strategies (user control over laziness), module expressions (for combining modules), theories and views (for describing module interfaces). For the massively parallel RRM (Rewrite Rule Machine). OBJ arose around 1976 as an executable formal notation for abstract data types with subsorts. Initial algebra semantics is executed by interpreting equations as rewrite rules. OBJ can be considered an implementation of Clear for the conditional order-sorted equational institution, since it supports both initial and loose semantics, as well as powerful generic modules and module inheritance; OBJ also makes explicit and extends the notion of module expression which was implicit in Clear. Viewed as a programming language, OBJ is first order and purely functional. The style of programming that results from the systematic use of generic modules and module expressions is called parameterized programming People: Structures: Related languages
References: Some History OBJ was originally designed in 1976 by Joseph Goguen as a language for "error algebras", an attempt to extend algebraic abstract data types to handle errors and partial functions in a simple, uniform way. This first design also used ideas from Clear for parameterized modules. Initial implementations of OBJ were done from 1977 to 1979 at UCLA by Joseph Tardo as OBJ0 and OBJT using error algebras plus an "image'' construct for parameterization. David Plaisted implemented OBJ1 by enhancing OBJT, during 1982-83 at SRI; improvements included (an efficient form of) matching modulo associativity and/or commutativity, hash coded memo functions, and a highly interactive environment. OBJ2 was implemented during 1984-85 at SRI by Kokichi Futatsugi and Jean-Pierre Jouannaud, following a design led by Joseph Goguen and Jos'e Meseguer, based on order sorted algebra rather than on error algebra; also, OBJ2 provided Clear-like parameterized modules, theories and views, although not in full generality. The latest version, OBJ3, is available from SRI International, and was developed (using Kyoto Common Lisp) by Joseph Goguen, Jos'e Meseguer, Timothy Winkler, Claude and H'el`ene Kirchner, and Aristide Megrelis; the implementation team was led by Jos'e Meseguer. Although OBJ3 has a syntax quite close to that of OBJ2, it has a different implementation based on a simpler and more efficient operational semantics for order sorted algebra. Also, it provides much more sophisticated module expressions, including default views, for which Timothy Winkler deserves special credit. OBJ can be seen as an implementation of Clear for conditional order sorted logic. Other implementations of OBJ include UMIST-OBJ from the University of Manchester Institute of Science and Technology, Abstract Pascal from the University of Manchester, MC-OBJ from the Univeristy of Milan, and a Franz Lisp OBJ2 from Washington State University. The first two are written in Pascal and the third in C. UMIST-OBJ is available in Britain as a commercial product, called Obj-Ex, and another variant, called Axis, is available from Hewlett- Packard Labs in Bristol, UK. In addition, we are extending OBJ in the directions of relational and object-oriented programming, to languages called Eqlog and FOOPS, respectively. The experimental OBJ systems implemented so far have been used for many applications, including debugging algebraic specifications, rapid prototyping, defining programming languages in a way that immediately yields an interpreter, specifying software systems, and hardware specification, simulation and verification. Many of these applications were produced under an experiment sponsored by the British Alvey Project, and will be collected with some more recent work in a book on the practical use of OBJ. OBJ is also being combined with Petri nets, thus allowing structured data in tokens, and is one language for programming a massively parallel machine that executes rewrite rules directly; in fact, we believe that OBJ on such a machine should greatly out-perform a conventional language on a conventional machine, by direct concurrent execution of rewrite rules; however, FOOPS offers some further advantages. Abstract: It is often claimed that the essence of functional programming is the use of functions as values, i.e., of higher order functions, and many interesting examples have been given showing the power of this approach. Unfortunately, the logic of higher order functions is difficult, and in particular, higher order unification is undecidable. Moreover (and closely related), higher order expressions are notoriously difficult for humans to read and write correctly. However, this paper shows that typical higher order programming examples can be captured with just first order functions, by the systematic use of parameterized modules, in a style that we call parameterized programming. This has the advantages that correctness proofs can be done entirely within first order logic, and that interpreters and compilers can be simpler and more efficient. Moreover, it is natural to impose semantic requirements on modules, and hence on functions. A more subtle point is that higher order logic does not always mix well with subsorts, which can nonetheless be very useful in functional programming by supporting the clean and rigorous treatment of partially defined functions, exceptions, overloading, multiple representation, and coercion. Although higher order logic cannot always be avoided in specification and verification, it should be avoided wherever possible, for the same reasons as in programming. This paper contains several examples, including one in hardware verification. An appendix shows how to extend standard equational logic with quantification over functions, and justifies a perhaps surprising technique for proving such equations using only ground term reduction. Extract: Introduction Following an introduction to the OBJ language, this paper gives some examples showing how higher order functions can be avoided by using sufficiently powerful parameterized modules. I do not consider higher order functions harmful, useless , or unbeautiful ; but I do claim significant advantages for avoiding higher order functions whenever possible, and I claim that they can be avoided quite systematically in functional programming, by using parameterized programming instead. Of course, higher order logic is useful in many areas, particularly the foundations of mathematics (e.g., type theory), extracting programs from proofs, describing proof strategies (e.g., LCF tactics), and the semantics of traditional programming languages (e.g., Scott-Strachey); but it too should be avoided whenever possible, and the appendix develops some techniques for reasoning about first order functions that often make it posssible to do so. Extract: Parameterized Programming Parameterized Programming A major advantage of functional programming over traditional imperative programming is that it can yield better structured programs [57]. However, a language with sufficiently powerful parameterized modules can achieve highly structured programs without higher order functions. In particular, the examples given below show that typical higher order functional programming techniques are easily carried out with OBJ's parameterized programming, in ways that seem to me even more structured and flexible. Code is broken into highly parameterized, mind-sized, internally coherent modules, and then new programs are constructed from old ones by instantiating, transforming and combining these modules. This paper argues that first order parameterized programming includes the essential power of higher order programming, and even offers certain advantages. Parameterized programming is a general and powerful technique for software design, production, reuse and maintenance. This approach involves abstraction through two kinds of module: objects to encapsulate executable code, and in particular to define abstract data types; and theories to specify both syntactic structure and semantic properties of modules. Each kind of module can be parameterized, where actual parameters are modules, and can also import other modules. Interfaces of parameterized modules are defined by theories, and thus include semantic as well as syntactic constraints 1 . For parameter instantiation, a view binds the formal entities in an interface theory to actual entities in a module, and also asserts satisfaction of the theory by the module. Views are first class citizens that can be named, can import modules, and can even be parameterized. This integration of objects, theories and views provides a powerful wide-spectrum capability. A software design is represented as a hierarchy of modules with associated views, and a software system is actually constructed from its components when the design (i.e., the code) is executed. In particular, module expressions allow complex instantiations of generics, and include commands that transform already defined modules; they can be seen as generalizing the unix make command. Maintenance is facilitated by editing and then re-executing such designs. Reusability is enhanced by the flexibility of the parameterization, composition and transformation mechanisms. Default views can greatly reduce the effort of defining views. All these ideas are illustrated in OBJ, a wide-spectrum, first order functional programming language that is rigorously based upon order sorted (conditional) equational logic. This logic provides a notion of subtype that supports many useful features, including multiple representation, overloading, coercion, multiple inheritance, and exception handling. This rigorous semantic basis allows a declarative, specificational style of programming, eases system design and implementation, and facilitates program verification. Moreover, logical specifications can be directly executed. These points are illustrated in several examples, including a simple hardware verification example. Extract: Aspects of OBJ Aspects of OBJ This section is a rather lengthy, but still incomplete and informal, introduction to OBJ. Readers already familiar with OBJ should skip directly to Section 3 and Appendix A. Readers who are already familiar with some other functional programming language should at least skim this section, because OBJ embodies basic design choices that are quite different from those of other programming languages, including other current functional programming languages: 1. It is rigorously based on deduction in order sorted equational logic, which provides a precise semantics for exception handling, multiple inheritance, overloading, and multiple representations for data abstractions. It uses strong sorting with retracts to ease parsing. 2. It supports parameterized programming, as sketched above and expanded below. 3. It supports user-defined evaluation strategies for each operation separately, rather than imposing a global order of evaluation; this allows both eager and lazy evaluation, as well as more complex options; also, efficient default evaluation strategies are computed by simple strictness analysis if the user does not provide an explicit strategy. 4. It has rewriting modulo attributes, including associative, commutative, identity and idempotent. OBJ is a logical programming language in the sense that it is based on inference in a precise logical system, namely conditional order sorted equational logic. As has been well argued by advocates of Prolog, this confers certain important benefits: program simplicity and clarity (which can greatly ease program understanding, debugging and maintenance); separation of logic and control; and identity of program logic with proof logic. In such a language, a high level description of what a program does actually is a program; that is, one can execute it. Other logical programming languages include pure Prolog, pure Lisp, and CDS; such languages can also be considered as efficiently executable specification languages. Some other languages that are based on algebraic semantics include Larch, Asspegique, Obscure and Act One; it seems fair to say that they have all been significantly influenced by OBJ. Higher order functional programming languages like Hope, Miranda, ML and Haskell can be seen as either based on rewrite rules, or else on higher order equational logic, although they tend to have some impure features for efficiency or convenience; for example, ML has assignment and exceptions, while Miranda has ad hoc coercions among various kinds of numbers, as well as lazy pattern matching. Standard ML has a powerful parameterized module facility inspired in part by Clear's. Guttag, Horowitz and Musser describe a system for the symbolic execution of algebraic abstract data types, and Levy and Sirovich describe the TEL system for specifying semantics with equations. Other related systems include those due to Hoffmann and O'Donnell, Lucas and Risch, and Prywes, all of which are first order, and the elegant work of Backus, which is higher order functional programming for a fixed set of rewrite rules and data types. This section provides an intuitive introduction to features of OBJ that are needed for understanding our higher order programming examples. Some important topics are thus omitted, including user-definable evaluation strategies, details of OBJ semantics, and default views. in IFIP Working Conference, 1977 Formal Description of Programming Concepts, North-Holland Pub. Co. 1978 view details in Theory and Practice of Software Technology, edited by D. Ferrari, M. Bolognani, and J. Goguen, North-Holland, 1982 view details in Theory and Practice of Software Technology, edited by D. Ferrari, M. Bolognani, and J. Goguen, North-Holland, 1982 view details Extract: Introduction Introduction Logic programming ([Kowalski 79]) attempts to improve programmer productivity by proposing logic, a human-oriented language, as a programming language. PROLOG, the flagship of logic programming languages, based on a resolution proof system, has a restricted syntax. TABLOG is based on a more flexible theorem prover, the deductive-tableau proof system ([Manna and Waldinger 80]), which allows a more intuitive and a richer syntax. A TABLOG program is a list of assertions, in (quantifier-free) first-order logic with equality. The execution of a program corresponds to the proof of a goal, which produces the desired output(s) as a side effect. Since a particular procedure is specified by the programmer, and since the proof taking place is always a proof of a special case of a theorem, viz., the case for the given input, the program interpreter does not need all the deduction rules available in the original deductive-tableau proof system. The theorem prover can be more directed, efficient, and predictable than a theorera prover used for program synthesis or for other general-purpose deduction. Extract: Introduction OBJ is also related to logic programming. It is based, however, on the algebraic semantics of abstract data types and equational theory rather than on (resolution-based) theorem proving in first-order logic. OBJ1 is an advanced implementation of the language that allows parametrized and hierarchical programming. OBJ1 includes system features for convenience and efficiency; it uses one-way pattern matching to apply rewrite rules rather than two-way unification. [Goguen and Meseguer 84] describes EQLOG, the extension of OBJ to include unification and Horn clauses. in [ACM] Logic and Functional Programming, 1984 view details in Zelkowitz, Marvin (ed) Specification of Reliable Software, IEEE, 1979. view details in Subramanyan, V.P. and Birtwhistle, Graham [eds], "Current Trends in Hardware Verification and Automated Theorem Proving" Springer, 1989. view details in Subramanyan, V.P. and Birtwhistle, Graham [eds], "Current Trends in Hardware Verification and Automated Theorem Proving" Springer, 1989. view details in Subramanyan, V.P. and Birtwhistle, Graham [eds], "Current Trends in Hardware Verification and Automated Theorem Proving" Springer, 1989. view details 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: OBJ OBJ Order-sorted term rewriting provides the operational semantics for the language OBJ [...], so OBJ's functional sublanguage is intended to provide support for prototyping. Its sophisticated module language also provides some support for prototyping at the level of (horizontal) system structure. It has been successfully used for research and teaching in software design and specification, rapid prototyping, theorem proving, and hardware verification. 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: 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]. in Subramanyan, V.P. and Birtwhistle, Graham [eds], "Current Trends in Hardware Verification and Automated Theorem Proving" Springer, 1989. view details in [ACM] ACM Computing Surveys (CSUR) 30(2) June 1998 view details in [ACM] ACM Computing Surveys (CSUR) 30(2) June 1998 view details |