Vienna Definition Language(ID:598/vie001)Formal language description language - Country: de
- Began: 1965
- Published: 1966
- Type:Definition languages
- Sammet:SPC
IBM Vienna Labs. A language for formal definition via operational semantics. Used to specify the semantics of PL/I.
Also VDL
People:
Related languages| ISWIM | => | Vienna Definition Language | | Influence | | PL/I | => | Vienna Definition Language | | Spec written in | | | | Vienna Definition Language | =>Base Language | Incorporated features of | | | | Vienna Definition Language | =>PLEASE | Influence | | | | Vienna Definition Language | =>Proxy | Influence | | | | Vienna Definition Language | =>System/A | Spec written in | | | | Vienna Definition Language | =>VDM-SL | Evolution of |
References:
1966- PL/I-Definition Group of the Vienna Laboratory "Formal Definition of PL/I (U.L.D. No. 3)" Tech. Rep. TR 25.071, IBM Laboratory Vienna, Vienna, Austria, Dec. 1966. view details
- Zemanek, H. "Semiotics and programming languages" pp139-143 view details DOI
in [ACM] CACM 9(03) March 1966 includes proceedings of the ACM Programming Languages and Pragmatics Conference, San Dimas, California, August 1965 view details
1969- Lucas, P. and Walk, K "On the formal description of PL/I" view details
in Halpern, Mark I and Shaw Christopher J (eds) "Annual Review in Automatic Programming" (6) 1969 Pergamon Press, Oxford view details
1970- Hoare, C. A. R. Review of Lucas and Walk 1969 in Computer Journal 13(2) 1970 p171
view detailsAbstract: Part 3 of this volume contains just one paper: "On the formal
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.
1971- Neuhold, E. J. "The Formal Description of Programming Languages," pp86-112 view detailsAbstract: This paper presents a formal method for describing programming languages independently of machine architectures and compiler implementations. The method, which was developed to describe PL/1, is being applied to other programming languages and to compilers and operating systems. The definitional techniques are demonstrated using a simple programming language (SPL). The paper has been written so that little knowledge of mathematics or formal logic is required. External link: Online copy at IBMExtract: Oriigns and Nature of the VDM language
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
19721973- Stock, Marylene and Stock, Karl F. "Bibliography of Programming Languages: Books, User Manuals and Articles from PLANKALKUL to PL/I" Verlag Dokumentation, Pullach/Munchen 1973 642 view detailsAbstract: PREFACE AND INTRODUCTION
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
1976- Pagan, FG "On interpreter-oriented definitions of programming languages" view details
in The Computer Journal 19(2) May 1976 view details - Todd, S. J. P. "The Peterlee relational test vehicle - a system overview" view detailsExtract: VDL and PRTV
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
1978- D. Bjorner, C.B. Jones "The Vienna Definition Method - The Metalanguage" view details
in Bjorner, D. et al eds, "The Vienna Development Method: The Meta- Language", LNCS 61, Springer 1978. view details
1980- Jones, C.B. "Software Development - A Rigorous Approach" Prentice Hall, Englewood Cliffs, NJ 1980
view details
1981- P. Lucas, "Formal Semantics of Programming Languages: VDL," IBM J. Res. Develop. 25,549-561 (1981).
view details
- Sammet, Jean E. "History of IBM's Technical Contributions to High Level Programming Languages" pp520ff
view details
in IBM Journal of Research and Development, 25(5), September 1981 25th anniversary issue view details
1982- Pagan, F. C. review of Lucas 1981 in ACM Computing Reviews September 1982
view detailsAbstract: Like most of the other papers in this 25th Anniversary Issue, this paper offers a mainly historical account (a "retrospective contemplation," in the author"s words) of its topic. It contains nothing new for anyone already familiar with the formal semantics field, but should be useful to the non-expert seeking to gain an overview of the area. Lucas describes in informal and largely nontechnical terms the background, concepts, and techniques of the Vienna Definition Language, a well-known metalanguage for specifying the operational semantics of programming languages. He also discusses the relation between VDL and some of the more recent work on denotational semantics and axiomatic semantics. The paper is well-supplied with 52 literature references.
- Smillie, K W. review of Sammet 1981 in ACM Computing Reviews September 1982 view detailsAbstract: This paper gives an assessment of the contributions of IBM to the development of programming languages. It begins with a very brief survey of the development of programming languages in order to place the work of IBM in perspective, followed by a few remarks on Speedcoding and PRINT, two very early attempts within IBM to develop programming languages. The four languages considered by the author to be major contributions by IBM are FORTRAN, GPSS, APL, and PL/I. The summary of the development of these languages is based primarily on the papers presented at the History of Programming Languages Conference in Los Angeles in 1978, and will be familiar to the readers of either the Preprints or the Proceedings of this conference. Several other languages -- Commercial Translator, FORMAC, SCRATCHPAD, QUIKTRAN, and CPS -- which have made important but lesser contributions are discussed briefly. A few remarks are made on IBM"s contribution to the syntactic and semantic description of languages with Backus-Naur Form and the Vienna Definition Language, respectively. There is a list of 58 references.
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.
1986- Jones, C.B. "Systematic Software Development Using VDM" Prentice Hall, Englewood Cliffs, NJ 1986 view details
- Terwilliger, Robert B. and Campbell, Roy H. "PLEASE:Predictable Logic based ExecutAble SpeCifications" Proceedings of the fourteenth annual ACM Annual Computer Science Conference Cincinnati, Ohio, United States 1986 pp349-358 view detailsExtract: Introduction
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.
1987- Bjorner, D. et al. (Eds.) "VDM '87: Vienna Definition Method - A Formal Method at Work" Proc. of a Symposium in Brussels March 1987. LNCS 252. Springer Berlin 1987; view details
1994- Zemanek, H.: "Early Foundations of Formal Modelling and Language Specification - VDL and VDM" pp251-270 view details
in Proc. IFIP Congress 94, North Holland Amsterdam, 1994. view details
|