CONTENTS & ABSTRACTS

In English. Summaries in Estonian

Proceedings of the Estonian Academy of Sciences.

Physics * Mathematics

Volume 52 No. 4 December 2003

Special issue on programming theory

NWPT’02

Foreword; 335–336

Jüri Vain and Tarmo Uustalu

On the category of data dependency algebras and embeddings; 337–355

Alexa Anderlik and Magne Haveraaen

Abstract. Programming a parallel computer is basically embedding the data dependency pattern of the program into the space-time pattern of the computer. In general this is a technically demanding task. By considering these patterns as algebraic structures – data dependency algebras and space-time algebras (a special case of data dependency algebras), we get a means for doing formal reasoning about the embedding problem, detached from concrete programs and machines. In this paper we show that it is possible to factorize data dependency algebras so that the embedding of a program into a parallel computer may be broken down to embeddings of simpler data dependency algebras into simpler space-time algebras. These simpler embeddings are then automatically combined to form a full embedding of the parallel program on the machine.

Key words: data dependency algebras, space-time embeddings, modularity, parallel programming, category of data dependency algebras.

Labelled BNF: a high-level formalism for defining well-behaved programming languages; 356–377

Markus Forsberg and Aarne Ranta

Abstract. The grammar formalism Labelled BNF (LBNF) and the compiler construction tool BNF Converter are introduced. Given a grammar written in LBNF, the BNF Converter produces a complete compiler front end (up to, but excluding, type checking), i.e. a lexer, a parser, and an abstract syntax definition. Moreover, it produces a pretty-printer and a language specification in LaTeX, as well as a template file for the compiler back end.

A language specification in LBNF is completely declarative and therefore portable. It reduces dramatically the effort of implementing a language.~The price to pay is that the language must be “well-behaved”, i.e. that its lexical structure must be describable by a regular expression and its syntax by a context-free grammar.

Key words: compiler construction, parser generator, grammar, Labelled BNF, abstract syntax, pretty-printer, document automation.

Extracting high-level information from Petri nets: a railroad case; 378–393

Thor Kristoffersen, Anders Moen, and Hallstein Asheim Hansen

Abstract. We show how useful simulation and control applications can be built on Petri nets by adding an object-oriented transformation framework called “views”. Petri nets were integrated into the Common Lisp Object System in such a way that the usual object-oriented features, such as classes, object creation, encapsulation, and inheritance, also work for Petri nets. This modified object system allows views to be implemented as collections of methods on the modified classes. Views are used to extract and present relevant domain-specific aspects of a Petri net model. This functionality was implemented in our prototype Petri net engine called Andromeda. As a test case we modelled the Oslo subway as a hierarchy of railroad specific components, and built a composite view showing train and passenger movements.

Key words: coloured Petri nets, simulation, object-orientation, formal modelling.

Fairness in automata theoretic model checking; 394–412

Tuomo Malinen and Matti Luukkainen

Abstract. We describe and perform empirical evaluation of two different methods for taking fairness assumptions into account in automata theoretic model checking. Both of the methods are known from the literature, even though they have not been presented in this form before. One of these methods is based on incorporating the fairness assumption into the system model; in the other one the fairness assumption is taken care of algorithmically. The goal of this work is to put these methods together, present them in a unified formal framework, and to compare their relative usefulness in some problems.

Key words: automata theory, model checking, Büchi automata, fairness, verification.

Global invariants for analysing multi-threaded applications; 413–436

Helmut Seidl, Varmo Vene, and Markus Müller-Olm

Abstract. We exhibit an interprocedural framework for the analysis of multi-threaded programs based on partial invariants of a new kind of constraint systems which we call side-effecting. We explore the formal properties of these constraint systems and provide general techniques for computing partial invariants. The practicality of this approach is demonstrated by designing and implementing a reasonably efficient flow- and context-sensitive interprocedural data-race analyser of multi-threaded C.

Key words: program analysis, multi-threading, constraint solving.

Erratum: High-temperature atomic layer epitaxy of TiO₂ from TiCl₄ and H₂O₂–H₂O (Proc. Estonian Acad. Sci. Phys. Math., 2003, 52, 3, 257–265); 437

Ahti Niilisk, Arnold Rosental, Aivar Tarre, and Teet Uustare

Instructions to authors; 438–440

Copyright Transfer Agreement; 441

Contents of volume 52; 442–444