Vienna Definition Language(ID:598/vie001)Formal language description languageIBM Vienna Labs. A language for formal definition via operational semantics. Used to specify the semantics of PL/I. Also VDL People: Related languages
References: in [ACM] CACM 9(03) March 1966 includes proceedings of the ACM Programming Languages and Pragmatics Conference, San Dimas, California, August 1965 view details in Halpern, Mark I and Shaw Christopher J (eds) "Annual Review in Automatic Programming" (6) 1969 Pergamon Press, Oxford view details description of PL/l' by P. Lucas and K. Walk. 'This paper presents the tools and the design criteria for the formal description of programming languages. The results reported were achieved mainly during the development of the formal definition of PL/l as documented in a series of technical reports (published by IBM Laboratory, Vienna). An appropriately tailored subset of PL/1 is used to illustrate these results. Their applicability is, however, not restricted to PL/l.' (quoted from first paragraph). The paper must be heartily welcomed as the first public manifestation of the valuable and original work which has been carried out over a period of some five years in the IBM Laboratory at Vienna. It is recommended as a useful general overview of the subject, suitable as an introduction for a reader with some inclination towards formal studies and at least a nodding acquaintance with PL/1. At the same time, it must be recognised that it is impossible to convey any full understanding of the properties of the 'Vienna' method and its application to PL/l within the limits of a monograph. Like Gibbon's 'Decline and Fall', the true nature of the achievement can only be appreciated after completing the entire work in unabridged form. The reason for this is plain. The purpose of a formal language definition is to be complete-to fill all the 'gaps' that may be left in an informal description. A formalisation which appears to be partially complete can be wholly unsatisfying. And yet very few who embark on the complete work will ever finish it. The main problem seems to me that the human reader does not take kindly to very large sets of definitions and axioms; he has an urgent need for worked examples and proofs. After all, even Gibbon has his jokes, and Shakespeare his comic relief. It is much to be hoped that the authors will have an opportunity to present their work more completely, with more concession to human weakness, between the covers of a book. in Halpern, Mark I and Shaw Christopher J (eds) "Annual Review in Automatic Programming" (6) 1969 Pergamon Press, Oxford view details The description of programming languages involves both the definition of the functions that can be expressed in the language (its semantics) and the notational rules governing the format to be used for requesting the functions (its syntax). A number of formal description methods exist for representing the syntax of programming languages,'*2'6 but natural language (such as English) is still generally used to specify their semantics. We describe one technique that allows the complete formal description (syntax and semantics) of programming languages. The principal features of this definitional method were developed for the formal description of The publications of J. McCarthy, P. J. Landin, and C. C. Elgot strongly influenced the early work leading to development of this method. So far, it has been used to at least partially describe ALGOL 60,15 FORTRAN, APL, and BASIC, as well as PL/l. Efforts are also underway to apply the techniques to compilers and to operating systems. The use of formal description methods allows programming languages to be defined in precise, universally understood terms, independently of machine architecture and compiler implementations. Such methods are also opening the way to further theoretical investigations of programming languages and compilers. The formal description method discussed in this paper is based on the notion that interpretive execution of a program in fact constitutes a semantical description of that program. In this case, the interpretation is conceptual rather than actual, the programs being interpreted are abstract rather than real, and the interpretation must be seen as applying to the entire language rather than a subset of its statements included in a particular program. The interpretation is performed by an abstract interpreter or abstract machine, which is not written in any programming or machine language but is specified in an artificial language based on abstract concepts of computing. The basic interpreter mechanisms are the same for all programming language definitions. However, for each language, different information must be kept during interpretation (values of variables, intermediate results, flow of control information) and different ways must be employed for handling this information (transfers of control, movements of data, procedure calls, arithmetic operations). Thus, formal language definition is concerned primarily with defining both the information to be retained by an abstract interpreter and the instructions and functions to be used by the interpreter in manipulating that information. By interpreting an abstract form of a program, the interpretation process is not burdened with purely notational considerations, such as spacing requirements, choice of separators and delimiters, and parentheses requirements and priority rules in arithmetic expressions. Abstract programs are defined using the abstract syntax of the programming language, which is designed to exhibit only those structural aspects of programs that are relevant to their interpretation. Thus the formal description of a programming language must include the specification of a translator that describes the mapping of source programs into their abstract form before interpretation. Finally, to complete the description, the formal syntax (using Backus-Naur Form) of well-formed source programs must be supplied at some stage in the production of the formal description. This paper is intended to provide a precise but not excessively formal presentation of the principles used for the complete formal description of programming languages. We develop a formal description of a simple programming language (SPL) as a vehicle for demonstrating the method. SPL has deliberately been kept very simple to avoid burdening the reader with learning a programming language as well as the formal description concepts. We have attempted to write the paper so that little knowledge of abstract mathematical or logical concepts is needed. However, at least a superficial knowledge of Backus-Naur Form notation is required. Some of the definitions we introduce differ from those used in the These changes were made partially to simplify the definitional technique itself and partially to simplify explanations; however, they do not fundamentally alter the descriptive method. in IBM Systems Journal 10(2) (Non-topical issue) 1971 view details in Computers & Automation 21(6B), 30 Aug 1972 view details in ACM Computing Surveys 4 March 1972 view details in ACM Computing Surveys 4 March 1972 view details The exact number of all the programming languages still in use, and those which are no longer used, is unknown. Zemanek calls the abundance of programming languages and their many dialects a "language Babel". When a new programming language is developed, only its name is known at first and it takes a while before publications about it appear. For some languages, the only relevant literature stays inside the individual companies; some are reported on in papers and magazines; and only a few, such as ALGOL, BASIC, COBOL, FORTRAN, and PL/1, become known to a wider public through various text- and handbooks. The situation surrounding the application of these languages in many computer centers is a similar one. There are differing opinions on the concept "programming languages". What is called a programming language by some may be termed a program, a processor, or a generator by others. Since there are no sharp borderlines in the field of programming languages, works were considered here which deal with machine languages, assemblers, autocoders, syntax and compilers, processors and generators, as well as with general higher programming languages. The bibliography contains some 2,700 titles of books, magazines and essays for around 300 programming languages. However, as shown by the "Overview of Existing Programming Languages", there are more than 300 such languages. The "Overview" lists a total of 676 programming languages, but this is certainly incomplete. One author ' has already announced the "next 700 programming languages"; it is to be hoped the many users may be spared such a great variety for reasons of compatibility. The graphic representations (illustrations 1 & 2) show the development and proportion of the most widely-used programming languages, as measured by the number of publications listed here and by the number of computer manufacturers and software firms who have implemented the language in question. The illustrations show FORTRAN to be in the lead at the present time. PL/1 is advancing rapidly, although PL/1 compilers are not yet seen very often outside of IBM. Some experts believe PL/1 will replace even the widely-used languages such as FORTRAN, COBOL, and ALGOL.4) If this does occur, it will surely take some time - as shown by the chronological diagram (illustration 2) . It would be desirable from the user's point of view to reduce this language confusion down to the most advantageous languages. Those languages still maintained should incorporate the special facets and advantages of the otherwise superfluous languages. Obviously such demands are not in the interests of computer production firms, especially when one considers that a FORTRAN program can be executed on nearly all third-generation computers. The titles in this bibliography are organized alphabetically according to programming language, and within a language chronologically and again alphabetically within a given year. Preceding the first programming language in the alphabet, literature is listed on several languages, as are general papers on programming languages and on the theory of formal languages (AAA). As far as possible, the most of titles are based on autopsy. However, the bibliographical description of sone titles will not satisfy bibliography-documentation demands, since they are based on inaccurate information in various sources. Translation titles whose original titles could not be found through bibliographical research were not included. ' In view of the fact that nany libraries do not have the quoted papers, all magazine essays should have been listed with the volume, the year, issue number and the complete number of pages (e.g. pp. 721-783), so that interlibrary loans could take place with fast reader service. Unfortunately, these data were not always found. It is hoped that this bibliography will help the electronic data processing expert, and those who wish to select the appropriate programming language from the many available, to find a way through the language Babel. We wish to offer special thanks to Mr. Klaus G. Saur and the staff of Verlag Dokumentation for their publishing work. Graz / Austria, May, 1973 in ACM Computing Surveys 4 March 1972 view details in The Computer Journal 19(2) May 1976 view details This is the earliest known application of VDL to database specification. The actual work was carriedout in the sunmer of 1974 when A. Hansal was an undergraduate student. The report gives a fairly complete and faithful model of the "Peterlee Relational Test Vehicle" (PRTV) - otherwise known as ISBL. PRTV is a relational algebra based DBMS actually implemented by the IBM UK Scientific Centre in the early 1970s. in IBM Systems Journal, 15(4), 1976 view details in Bjorner, D. et al eds, "The Vienna Development Method: The Meta- Language", LNCS 61, Springer 1978. view details in Bjorner, D. et al eds, "The Vienna Development Method: The Meta- Language", LNCS 61, Springer 1978. view details in Bjorner, D. et al eds, "The Vienna Development Method: The Meta- Language", LNCS 61, Springer 1978. view details in IBM Journal of Research and Development, 25(5), September 1981 25th anniversary issue view details in IBM Journal of Research and Development, 25(5), September 1981 25th anniversary issue view details The author is eminently qualified to have written this paper. She is a long-time employee of IBM, and has written many papers and a definitive book on the development of programming languages. Her account of the contributions of IBM to the development of programming languages is itself a contribution to the subject. in IBM Journal of Research and Development, 25(5), September 1981 25th anniversary issue view details in IBM Journal of Research and Development, 25(5), September 1981 25th anniversary issue view details Introduction It is widely acknowledged that producing correct software is both difficult and expensive. To help remedy this situation, methods of specifying and verifying software have been developed. The SAGA (Software Automation, Generation and Administration) project is investigating both the for real and practical aspects of providing automated support for the full range of software engineering activities. PLEASE is a language being developed by the SAGA group to support the specification, prototyping, and rigorous development of software components. In this paper we describe the development methodology for which PLEASE was created, give an example of development using the language, and describe the methods used to prototype PLEASE specifications. A life-cycle model describes the sequence of distinct stages through which a software product passes during its lifetime. There is no single, universally accepted model of the software life-cycle. The stages of the life-cycle generate software components, such as code written in programming languages, test data or results, and many types of documentation. In many models, a specification of the system to be built is created early in the lit%-cycle; as components are produced they are verified for correctness with respect to this specification. The specification is validated when it is shown to satisfy the customers requirements. Producing a valid specification is a difficult task. The users of the system may not really know what they want, and they may be unable to communicate their desires to the development team. If the specification is in a formal notation it may be an ineffective medium for communication with the customers, but natural language specifications are notoriously ambiguous and incomplete. Prototyping and the use of executable specification languages have been suggested as partial solutions to these problems. Providing the customers with prototypes for experimentation and evaluation early in the development process may increase customer/developer communication and enhance the validation and design processes. To help manage the complexity of software design and development, methodologies which combine standard representations, intellectual disciplines, and well defined techniques have been proposed. For example, it has been suggested that top-down development can help control the complexity of ~ program construction. By using stepwise refinement to create a concrete implementation from an abstract specification we divide the decisions necessary into smaller, more comprehensible groups. Methods to support the top-down development of programs have been devised and put into use. It has also been proposed that software development may be viewed as a sequence of transformations between specifications written at different linguistic levels; systems to support similar development methodologies have been constructed. Extract: VDM and PLEASE The Vienna Development Method supports the top-down development of programs specified in a notation suitable for mathematical verification. In this method, programs are first written in a language combining elements from conventional programming languages and mathematics. A procedure or function may be specified using pre and post-conditions written in predicate logic; similarly, an invariant ,nay be specified for a data type. Then these abstract programs are incrementally refined into programs in an implementation language. The refinements are performed one at a time, and each is verified before another is applied; therefore, the final program produced by the development satisfies the original specification. Extract: Path Pascal and PLEASE Path Pascal is an extension to standard Pascal allowing concurrent programming and encapsulated data types. In Path Pascal, a process is a program structure which has an independent thread of execution; independently executing processes communicate through shared data structures. Encapsulated data types called objects are manipulated only by the predefined routines associated with the type. Path expressions specify synchronization constraints that apply to the execution of the processes, functions and procedures within objects. Extract: about PLEASE PLEASE is an extension of Path Pascal, which supports a methodology similar to the Vienna Development Method. In PLEASE, a procedure or function may be specified with pre- and post-conditions written in predicate logic, and similarly an object may be specified using an invariant. For ease of expression, several data types have been added to the language. PLEASE specifications may be used in proofs of correctness; they also may be transformed into prototypes which use Prolog to "execute" pre- and post conditions, and may interact with other modules written in conventional languages. We believe that the early production of executable prototypes for experimentation and evaluation will enhance the software development process. Extract: Plan In section two of this paper, we describe the development methodology PLEASE was designed to support, and in section three, we give an example of program development using PLEASE. First we discuss an example program specification and describe how an executable prototype could be created for it. Then we show a refinement of this specification and discuss the process of verifying that the refined specification satisfies the original. In section four, we give an example of data type specification in PLEASE, and in section five, we discuss the implementation of the system, in section six, we describe tile work we have planned for the future and in section seven, we summarize and draw some conclusions from our experience. in IBM Journal of Research and Development, 25(5), September 1981 25th anniversary issue view details in IBM Journal of Research and Development, 25(5), September 1981 25th anniversary issue view details in Proc. IFIP Congress 94, North Holland Amsterdam, 1994. view details |