A formal notation for specifying static semantic rules

The syntax rules of programming language are generally fairly well understood and may easily be expressed formally as a grammar using BNF. However, the static semantic rules are less well understood and considerably more difficult to express formally. All notations for expressing static semantic rules either formally or informally involve actions being associated with the productions of the grammar. This paper presents such a formal notation which has been applied to various languages and found to be very useful both for the designer and the compiler writer.     

Methods for specifying static semantics

The formal specification of a programming language involves the specification of three types of rules: syntax, static semantics and semantics. Various methods have been proposed for specifying the static semantic rules of programming languages, but as yet no method has received general acceptance. This paper looks at several different specification techniques and attempts to isolate the basic mechanisms used by each of them and explain the pattern of development of specification techniques for static semantics.     

A methodology and notation for compiler front end design

A methodology and associated notation for designing compiler front ends, and in particular the interface between the parser and the semantic routines, is described. The methodology leads to a clean, easy to understand, documentable design. The notation is similar to an attribute grammar, but its purpose is to document the first pass of a specific compiler, rather than to describe the semantics of a language. It is designed to be accessible to non-specialists, easy to learn, and natural. It can be used with or without software support. The notation was used during the development of a large compiler, and to assist in the transfer of the compiler to the group that will maintain it. Experience with the notation indicates that it meets its goals.     

A demonstrably correct compiler

As critical applications grow in size and complexity, high level languages, rather than better-trusted assembly languages, will be used in their development. This adds potential for extra errors to creep in, especially in the now necessary compiler. To avoid these new errors, it is necessary to have a formal specification of the high level language, and a formal development of its compiler. We outline what we believe is a practical route for achieving a demonstrably correct compiler, and describe a prototype compiler we have built by this route for a small, but non-trivial, language.     

Deriving a compiler from an operational semantics written in VDL

This paper addresses the issue of compiler correctness. The approach taken is to systematically construct a correct compiler for a language from a formal semantic definition of the language. For this purpose, an operational semantics of a language is chosen as the basis for the approach. That is, the compiler for a language is derived from an interpreter of the language. The derivation process uses the notion of mixed computation proposed by Ershov. Briefly stated, one begins interpreting and when a primitive state changing instruction is about to be executed, the instruction is emitted as code instead. The correctness of all compilers produced by the method is guaranteed by proving the derivation rules correct. This proof is a one-time task for each specification language. The specification language studied in this paper is the Vienna Definition Language (VDL). The object code generated by the compiler is in an intermediate language close to an assembly language. Therefore, the translation from the intermediate language into the assembly language should be straightforward.     

A formal semantics of SMIL: a web standard to describe multimedia documents

This paper presents a formal semantics of a subset of SMIL2.0: a W3C recommendation to describe interactive multimedia documents on the Web. This work has been used during the design of this standard to improve its consistency. It is also intended to help SMIL developers to understand the specification. Doing so, it will contribute to increase SMIL chances of success in achieving the interoperability goal and, thus, its impact on the new information society.     

The design of a pascal compiler

The development of a compiler for the programming language PASCAL¹ is described in some detail. Design decisions concerning the layout of program and data, the organization of the compiler including its syntax analyser, and the over-all approach to the project are discussed. The compiler is written in its own language and was implemented for the CDC 6000 computer family. The reader is expected to be familiar with Reference 1.     

The UML as a formal modeling notation

The Unified Modeling Language (UML) is an Object Management Group (OMG) object-oriented (OO) modeling notation standard. It consists of a set of notations for modeling systems from a variety of views and at varying levels of abstraction. While the UML reflects some of the best OO modeling experiences available, it suffers from a lack of precise semantics that is necessary if one is to use the notations to precisely model systems and to rigorously reason about the models. In this paper we discuss some of the problems with the current UML semantic document and present the approach that the precise UML group (pUML) group is using to develop a precise semantics for the UML. The approach utilizes mathematical techniques to explore and gain insights into appropriate semantics for UML modeling concepts. The insights and formal expressions will then be used to develop a UML semantics document written in natural language that defines the semantics in a precise, consistent, and understandable manner.     

Equivalence of formal semantics definition methods

There are numerous methods of formally defining the semantics of computer languages. Each method has been designed to fulfil a different purpose. For example, some have been designed to make reasoning about languages as easy as possible; others have been designed to be accessible to a large audience and some have been designed to ease implementation of languages. Given two semantics definitions of a language written using two separate semantics definition methods, we must be able to show that the two are in fact equivalent. If we cannot do this then we either have an error in one of the semantics definitions, or more seriously we have a problem with the semantics definition methods themselves.Three methods of defining the semantics of computer languages have been considered, i.e. Denotational Semantics, Structural Operational Semantics and Action Semantics. An equivalence between these three is shown for a specific example language by first defining its semantics using each of the three definition methods. The proof of the equivalence is then constructed by selecting pairs of the semantics definitions and showing that they define the same language.A full version of this paper can be accessed via our web page http://www.cs.man.ac.uk/fmethods/ facj.html     

A formal semantics of nested atomic sections with thread escape

The multi-core trend is widening the gap between programming languages and hardware. Taking parallelism into account in the programs is necessary to improve performance. Unfortunately, current mainstream programming languages fail to provide suitable abstractions to do so. The most common pattern relies on the use of mutexes to ensure mutual exclusion between concurrent accesses to a shared memory. However, this model is error-prone and scales poorly by lack of modularity. Recent research proposes atomic sections as an alternative. The user simply delimits portions of code that should be free from interference. The responsibility for ensuring interference freedom is left either to the compiler or to the run-time system.In order to provide enough modularity, it is necessary that both atomic sections could be nested and threads could be forked inside an atomic section. In this paper we focus on the semantics of programming languages providing these features. More precisely, without being tied to a specific programming language, we consider program traces satisfying some basic well-formedness conditions. Our main contribution is the precise definition of atomicity, well-synchronisation and the proof that the latter implies the strong form of the former. A formalisation of our results in the Coq proof assistant is described.     

Applying abstraction and formal specification in numerical software design

Numerical software development tends to struggle with an increasing complexity. This is, on the one hand, due to the integration of numerical models, and on the other hand, due to change of hardware. Parallel computers seem to fulfill the need for more and more computer resources, but they are more complex to program.

The article shows how abstraction is used to combat complexity. It motivates that separating a specification, “what,” its realisation, “how,” and its implementation, “when, where,” is of vital importance in software development. The main point is that development steps and levels of abstraction are identified, such that the obtained software has a clear and natural structure.

Development steps can be cast into a formal, i.e., mathematical framework, which leads to rigourous software development. This way of development leads to accurate and unambiguous recording of development steps, which simplifies maintenance, extension and porting of software. Portability is especially important in the field of parallel computing where no universal parallel computer model exists.     

Steps towards a method for the formal modeling of dynamic objects

Fragments of a method to formally specify object-oriented models of a universe of discourse are presented. The task of finding such models is divided into three subtasks, object classification, event specification, and the specification of the life cycle of an object. Each of these subtasks is further subdivided, and for each of the subtasks heuristics are given that can aid the analyst in deciding how to represent a particular aspect of the real world. The main sources of inspiration are Jackson System Development, algebraic specification of data- and object types, and algebraic specification of processes.     

An analysis of Pascal programs in compiler writing

A method and results of static and dynamic analysis of Pascal programs are described. In order to investigate characteristics of large systems programs developed by the stepwise refinement programming approach and written in Pascal, several Pascal compilers written in Pascal were analysed from both static and dynamic points of view. As a main conclusion, procedures play an important role in the stepwise refinement approach and implementors of a compiler and designers of high level language machines for Pascal-like languages should pay careful attention to this point. The set data structure is one of the characteristics of the Pascal language and statistics of set operations are also described.     

Modeling multi-rate DSP specification semantics for formal transformational design in HOL

The CATHEDRAL Silicon Compilers synthesize hardware for DSP algorithms specified in Silage, a high level applicative language. In order to optimize the results of the silicon compilation in terms of chip-area and/or throughput, the user often massages the specification applying transformations to the Silage code. To guarantee that the transformations preserve the behavior of the specified algorithm, the formal semantics of the specification language had to be defined. The semantics has been used to prove in HOL the correctness of the transformations and to prove properties of the specification. We are currently building a system where a menu of useful andcorrectness preserving transformations will be available to the user. In this system the user could choose appropriate transformations from the menu taking advantage of his creativity and expertise to interactively guide the silicon compiler, without the risk of introducing inconsistencies. This article describes the formalmulti-rate semantics of a substantial subset of Silage and illustrates some formally verified transformations.     

A formal framework for design and verification of robotic agents

Intelligent robots are autonomous and are used in environments where human interaction is hazardous or impossible. Verification of software for intelligent robots is mandatory because in situations where intelligent robots are employed online, error recovery is almost impossible. In this paper, we provide a formal framework for offline verification of software used in robotic applications. The specification enables one to design a robotic agent which represents a class of real-life robots. Forward and inverse kinematic operations of the robotic agent are specified using the specification for rigid solids and their primitive operations. An object-oriented design of the robotic agent derived from the specifications is given. We use the specification technique VDM for our purpose.This work was partially supported by FCAR, Quebec and NSERC, Canada.     

Nivel: a metamodelling language with a formal semantics

Much work has been done to clarify the notion of metamodelling and new ideas, such as strict metamodelling, distinction between ontological and linguistic instantiation, unified modelling elements and deep instantiation, have been introduced. However, many of these ideas have not yet been fully developed and integrated into modelling languages with (concrete) syntax, rigorous semantics and tool support. Consequently, applying these ideas in practice and reasoning about their meaning is difficult, if not impossible. In this paper, we strive to add semantic rigour and conceptual clarity to metamodelling through the introduction of Nivel, a novel metamodelling language capable of expressing models spanning an arbitrary number of levels. Nivel is based on a core set of conceptual modelling concepts: class, generalisation, instantiation, attribute, value and association. Nivel adheres to a form of strict metamodelling and supports deep instantiation of classes, associations and attributes. A formal semantics is given for Nivel by translation to weight constraint rule language (WCRL), which enables decidable, automated reasoning about Nivel. The modelling facilities of Nivel and the utility of the formalisation are demonstrated in a case study on feature modelling.