From ADT to UML-like modeling

Egidio Astesiano, Maura Cerioli, Gianna Reggio

UML and similar modeling techniques are currently taking momentum as a de facto standard in the industrial practice of software development. As other Object Oriented modeling techniques, they have benefited from concepts introduced or explored in the field of Algebraic Development Techniques - for short ADT, formerly intended as Abstract Data Types - still an active area of research, as demonstrated by the CoFI project. However , undeniably, UML and ADT look dramatically different , even perhaps with a different rationale. We try to address a basic question: can we pick up and amalgamate the best of both? The answer turns out to be not straightforward. We analyze correlations, lessons and problems. Finally we provide suggestions for further mutual influence, at least in some directions.

BDDs and resolution cannot simulate each other polynomially

Jan Friso Groote

There is little understanding in how different proof search methods for propositional logic compare. And so, in this field new techniques to search proofs for propositional formulas are being proposed on a regular basis, and more remarkably, some of these perform unexpectedly well. Two of these proof search techniques that amazed the world in the last decades are binary decision diagrams (BDDs) and Stalmark's Prover (which is a form of resolution). We (Hans Zantema and I) have attempted to increase understanding in this field by proving that resolution and BDDs are fundamentally different techniques, in the sense that there are examples where proofs using one technique are exponentially shorter than proofs using the other and vice versa. This implies that none of the two is the preferred technique for propositional proof search. In this talk I will sketch the techniques, outline the proof and put all in a wider context.

The Abstract State Machine Paradigm: What is In and What is Out

Yuri Gurevich

The computing science is about computations. But what is a computation? We try to answer this question without fixing a computation model first. This brings up additional foundational questions like what is a level of abstraction? The analysis leads us to the notion of abstract state machine (ASM) and to the ASM thesis:

Let A be any computer system at a fixed level of abstraction. There is an abstract state machine B that step-for-step simulates A.

In the case of sequential computations, the thesis has been proved from first principles; see ACM Transactions on Computational Logic, vol. 1, no. 1 (July 2000), pages 77-111. Of course ASMs are not necessarily sequential. In a distributed ASM, computing agents are represented in the global state. New agents can be created, and old agents can be deactivated. There could be various relations among agents and various operations on agents. The global state is a mathematical abstraction different from the conventional shared memory; it may be, for example, that the agents communicate only by messages. The moves of different agents form a partially ordered set. Concurrent moves cause consistent changes of the global state.

Often a formal method comes with a reasoning system. If this is your idea of a formal method then the ASM approach is not a formal method. It is system informatics where modeling is carefully separated from formal reasoning. Notice that formal reasoning is possible only when the raw computational reality is given a mathematical form; ASMs do the modeling job.

The separation of modeling and reasoning concerns does not undermine the role of reasoning. The ASM approach is not married to any particular formal reasoning system and is open to all of them. It is usual for ASMs to have integrity constraints on states. ASM programs can be enhanced with various pre and post conditions. ASM-based testing can be enhanced with model checking. The most important direct application of ASMs is their use as executable specifications. This makes (totally as well as partially) automated reasoning relevant.

For more information on abstract state machines see the academic ASM website.

From Play-In Scenarios to Code: An Achievable Dream

David Harel

High-level modeling of complex reactive systems raises rather serious problems in specifying behavior. This is true when working within either the structured analysis paradigm (SA) or the object-oriented one (OO). Models must remain intuitive and well-structured, but also behaviorally expressive and rigorous, supporting full executability and dynamic analysis, as well as automatic generation of usable code in languages such as C, Java or C++. The talk will be high-level in spirit, and somewhat "philosophical", summarizing better-known and less-known ideas. It will center on a general system development scheme, supported by semantically rigorous automated tools, within which one can go from a high-level, user-friendly requirement capture method, which we call "play-in scenarios", to a final implementation. A cyclic process consisting of verification against requirements, and synthesis from requirements, plays an important part in the scheme.

At the edge of Design by Contract

Bertrand Meyer

Combining the Hoare-Dijkstra concepts of assertions and systematic software construction with principles of object technology and data abstraction, Design by Contract provides a solid basis for building, testing, documenting and maintaining quality O-O software. This presentation will examine issues at the forefront of Design by Contract, including a number of problems to which no answer is known at the moment, covering in particular the areas of program correctness, component validation, and concurrency.

What Use is Formal Semantics?

Peter D. Mosses

Formal descriptions of syntax are quite popular: regular and context-free grammars have become accepted as useful for documenting the syntax of programming languages, as well as for generating efficient parsers; regular expressions are extensively used for searching and transforming text. Formal semantic descriptions, in contrast, are widely regarded as only of academic interest, and they have so far found little application in practical software development.

In this talk, we survey the main frameworks for formal semantics: operational, denotational, and axiomatic semantics, together with some more recent hybrid approaches. We assess the potential usefulness of descriptions in the various frameworks, considering also their practical aspects, such as comprehensibility, modularity, and extensibility, which are especially significant when describing full-scale languages. Finally, we argue that formal semantics will never be regarded as truly useful until tools become available for transforming semantic descriptions into efficient compilers and interpreters.

The audience is assumed to be familiar with the basic concepts of operational and denotational semantics.

A.A.Liapunov and A.P.Ershov in the theory of program schemes and the development of its logic concepts

Rimma Podlovchenko

The aim of this paper is to survey the advent and maturation of the theory of program schemes, emphasize the fundamental contributions of A.A.Liapunov and A.P.Ershov to this branch of computer science, and discuss the main trends in the theory of program schemes. The paper is organized as follows.

1. Aleksei Andreevich Liapunov and his influence on the scientific interests of Andrei Petrovich Ershov. We cast a look in the 1950s when theoretical computer science left its cradle and made first steps. It was the time of A.P.Ershov's studentship. We recall the excitement of scientific work of that time, daring intentions of young researchers that formed the landscape of the present-day computer science.
2. The advent of the theory of program schemes. The main cause of passing from computer programs to their schemes was the strong intention to develop equivalent transformations (optimizations) of programs by using program schemes for abstract formal models of real computer programs. This is the principal context in which the basic concepts and results of the theory of program schemes are reviewed in this talk. The first achievements of this theory include, among others, the results on formal models of computer programs.
3. On the methodological contribution of A.P.Ershov to the theory of program schemes.} We give a brief survey of the key concepts, notions, methods and godsends introduced by A.P.Ershov in the theory of program schemes and focus mostly on his contribution to:

• Foundation of formal methods in computer science as a tool for developing equivalent transformations of computer programs. A.P.Ershov proposed several formal models of sequential computer programs, indicated the main problems in the selection and analysis of these models and outlined the basic methods of their attacking.
• Development of the theory of program schemes. Two fundamental problems are tackled in this theory: the equivalence problem and the equivalent transformation problem for program schemes. The latter consists in the development of systems of equivalent transformations that are complete in the specific classes of program schemes.

4. Evolution of the theory of algebraic models of computer programs. This is a relatively novel branch in the theory of program schemes. We point out the main results and crucial points in the development of this branch of theoretical computer science and concentrate our attention on two fundamental problems mentioned above.
5. Current trends in the theory of program schemes. We present some new lines of attacking the equivalence and the equivalent transformation problems for program schemes. One of the new approaches to the equivalence problem is being developed by V.Zakharov. His methods continue the earlier ideas and techniques worked out by A.Letichevsky. Another approach has been advanced by R.Podlovchenko. Its key idea is to check the equivalence of program schemes by computing and analyzing invariants based on their structure. Both methods make it possible to design efficient equivalence-checking algorithms. In addition to this, the second method is also applicable to the solution of the equivalent transformation problem for program schemes.
6. Resume. The theory of algebraic models of computer programs clearly demonstrates the fruitfulness of the basic concepts of the theory of program schemes. These models quite naturally fit a number of models of computations.

Rimma I. Podlovchenko
Science Research Computer Center
Moscow state University, RU-119899, Russia
rip@vvv.srcc.msu.su

A.P. Ershov - a pioneer and leader of programming in Russia

Igor Pottosin

Andrei Ershov belonged to the first generation of native programmers. He was among the first University graduates in programming (Moscow State University, 1954). Programming as a profession appeared two years earlier and formed from professional mathematicians and physicists. Taking into account the fact that Ershov became a programmer even in his student years, it is possible to say that he shared the way of programming as a profession and scientific discipline.

Being a pioneer of programming, he passed through all stages of evolution of programming - from a tool for solution of numerical problems to formation of the first independent research fields in programming, such as compilers and languages, operating systems and theoretical models of programs. Like all programmers of the first generation, Ershov has felt all the difficulties and problems connected with formation of a new scientific direction - it was necessary to prove that this direction has the right to exist, has its own scientific value and its problems are as important and essential as the foundations of already formed scientific disciplines. This can be illustrated by the hard history of Ershov's works on operator algorithms, one of the models of program schemata and difficulties with the Alpha-project.

A.Ershov was not just one of the participants of the formation process of a new discipline, he became one of its leaders. His leading role in this direction is out of discussion. It is sufficiently to note the importance of his works and results for self-identification of the new scientific direction.

Ershov was one of the creators of the compilation theory and methodology - the initial research area in programming. Creation of a general, language-independent compilation scheme, the concept of internal representation abstracted from semantic properties of a program, creation of a number of techniques, such as hash functions, memory allocation technique and so on - such were his results in this field. He is the author of the first monograph on program compilation (A.P. Ershov. Programming Program for the BESM Computer. Pergamon Press, London, 1959).

He made an essential step in post-Algol evolution of programming languages: the Alpha-language, an extension of Algol-60, had such properties as multi-dimension variables, various do-statements, initial values and so on. The Sigma language proposed by Ershov was an example of a language kernel extended by substitution mechanism.

The foundation of programming originated from the experience of implementation of real programming systems, was based on this experience. Ershov's leadership was also evident in the fact that he was either an initiator or a supervisor (or both) of a number systems of fundamental importance each of which was based on new ideas and approaches. The most important of them are as follows: the Alpha-project - the first programming system for Algol-like language with high-level program optimization; Aist-0 - a multiprocess and multiuser system with rich multifunctional software; the Beta-project - a multilanguage compiling system with implementation of popular programming languages (Pascal, Modula-2, Simula-67, Ada); the programming system Setl - implementation of one of the first specification language; the workstation Mramor - hardware and software support for publishing activity; the programming system Shkol'nitza - a methodologically grounded tool for school training in programming.

A.Ershov was one of the founders of the program schemata theory (see [1]). It is important to say that he always saw the relation between programming theory and programming practice. The examples of this are application of his memory allocation theory to implementation of memory optimization in the Alpha-system, initialization of research in constructing program models oriented to justification of program optimizations, the development of parallel program models as a part of general research in multiprocessing of Aist-0, and so on.

Mixed computation concept is one of his main results in this symbiosis of theory and practice. This concept, proposed by Ershov as a fundamental one for creation of language processors, became the basis for a number of real specialization systems for imperative and declarative languages.

One of the main problems of the new direction is training of professionals and researchers. Ershov was a pioneer in this field too. His great efforts in foundation of educational informatics, its methology, writing manuals and programming systems for education were very important. He was an absolute leader of this activity in our country.

He had a great influence on the spirit of this new field, its ethics, its professional specific. The social image of programming in our country was formed by activity of such organizations as the Commission on System Software, the Committee on Programming Systems and Languages, and the Council on Cybernetics headed by Ershov. His well-known papers "Two faces of programming", "Aesthetics and the human factors of programming", and "Programming, the second literacy" have defined the spirit and specific of a new kind of activity very brightly and clearly.

References

1. R.I.Podlovchenko. A.A.Liapunov and A.P.Ershov in the theory of program schemes and the development of its logic concept
2. D.Bjorner, V.Kotov (Eds). Images of Programming / North-Holland, 1991.
3. V.Kotov, I.Pottosine. Andrei P.Ershov 1931-1988 // Theoretical Computer Science, v. 67, № 1, 1989, P. 1-4.
4. W.M.Turski. Obituary: Andrei Petrovich Ershov // IEEE Annals of the History of Computing, v. 13, № 2, 1993, P. 55-58.

Igor V. Pottosin
A. P. Ershov Institute of Informatics Systems,
6, Acad. Lavrentjev pr.,
Novosibirsk 630090 Russia
ivp@iis.nsk.su