CIP-L(ID:1072/cip001)For Computer-aided Intuition-guided Programming. Wide-spectrum language for incremental program transformation. There are ALGOL-like and Pascal-like variants. People: Related languages
References: Introduction It seems reasonable to organize the activity of writing computer programs in the form of a development process leading through a series of more and more detailed versions. A number of ways for carrying out such developments have been suggested ranging from Wirth's "stepwise refinement" to Dijkstra's "discipline of programming." We consider here a most rigorous approach where the transition between the successive versions is done according to strictly formal rules called "program transformations." This idea took shape in the middle of the 1970's. At this time, several groups started a systematic research on the subject. In Munich, working plans for a project called CIP ("Computer-Aided Intuition-Guided Programming") were fixed in 1975 under the joint guidance of F. L. Bauer and K. Samelson after two years of exploration (cf. [ 1 ] ). This project comprises the design of an (abstract) programming language and of a support system for carrying out transformations. As a consequence of this approach programs are considered as formal objects ("formulas") which can be manipulated by transformation rules ("deduction rules"). These considerations lead to a sound mathematical basis for program transformations and their correctness. Of course, it is also important to discuss the software engineering aspects, i.e., questions concerning the methodology of software construction which allows us to make the best use of transformation techniques. This includes the problems of the transformation systems and the degree to which they shall provide automated support for the programmer. Such systems usually comprise catalogs of transformation rules, a manipulation system, a user interface, and possibly some kind of heuristics. However, in this paper we want to concentrate on the basic idea and the formal background of the program development by transformations. At first, the collection of examples appears to be random and without reason, but soon it becomes clear that each of the earlier examples is used to build at least one later, more substantial example. The examples are programmed nicely, but their descriptions are terse, probably in order to squeeze all the examples into the allotted pages. Sometimes the brief explanation of an example seems to require intimate knowledge of algebraic semantics. However, when studied carefully, the examples do work out to the reader's satisfaction. This reviewer found one remark of the paper curious. In Section 2.6, one reads " The interpreter is in many parts very inefficient. Useful first steps in developing this specification towards a real implementation would be to merge the context functions ... and to incorporate the context checks into the interpreter itself. " In its original form the specification clearly separates the context checks, which are to be done at translation time, from the interpretation, which is to be done at run time. It seems to this reviewer that moving the context checks into the interpreter will slow the interpreter down. In general, doing as much checking as possible at translation time, which occurs once, pays off in reduced interpretation time, which occurs many times. Even if one is not interested in the idea of a widespectrum language and its use in software development, the paper is worth reading for its concise specifications of a number of types and procedures. The types defined include Boolean, natural number, integer, finite set, partial and total finite mapping, array, sequence, stack, queue, deque, 3-expression, tree, and CIP-L semantic objects types. The procedures defined included a context-checker, an interpreter, a program transformer for CIP-L, and a modestsized text editor. in ACM Computing Reviews January 1983 view details in ACM Computing Reviews January 1983 view details in ACM Computing Reviews January 1983 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: 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: cip-l CIP-L is a wide spectrum language that was particularly designed for use within the transformational program development methodology. It offers constructs for all levels of program development, ranging from specification constructs via applicative constructs to notations for procedural and machine-oriented programs. For the purpose of formal specification, CIP-L offers a sub-language for algebraic specifications, as well as particular constructs such as set comparison, quantification, choice, and a mechanism for formulating descriptive expressions. The characteristics of the CIP-L sub-language for algebraic specifications are that it provides parameterized, hierarchically structured specifications, partial operations, first-order axioms and a loose semantics. 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 ACM Computing Reviews January 1983 view details |