Annotated Bibliography on Evolving Algebras

Egon Börger

Abstract:

It is intended to make current updates of this bibliography available for anonymous ftp as dvi-file, as compressed ps-file and as tex-file in the directory pub/Papers/boerger of the machine ftp.di.unipi.it. At the beginning of the tex-file it is indicated how the file can also be edited without the annotations. If you want to use the tex-file to compile your own references, note the following principle which has been used for defining the keys.

The key for a paper published in 1945 by (a single author) Bach is Bach45, i.e. the author's name, where the first letter is a capital, followed by the last two digits of the year of publication of the paper. The key for a paper with two authors, Bach and Beethoven, is BacBee45; if there is a third author, Brahms, it is BaBeBr45; with a fourth author, Bartok, it becomes BaBeBB45, etc.

The order of the references is alphabetical; it is chronological within a group of authors. If for a group of authors there is more than one paper in the one year 1945, these papers receive keys with suffix 45a, 45b, 45c etc.

Some of the papers mentioned in this bibliography can be obtained by anonymous ftp from the following machines in the indicated directory:

1. ftp.di.unipi.it, directory pub/Papers/boerger

2. ftp.eecs.umich.edu, directory /groups/Ealgebras

References

1

C. Beierle. Formal Design of an Abstract Machine for Constraint Logic Programming. In B. Pehrson and I. Simon (Eds.) IFIP 13th World Computer Congress 1994, Volume I: Technology/Foundations, Elsevier, Amsterdam, 377-382.

Proposes a general implementation scheme for CLP(X) over an unspecified constraint domain X by designing a generic extension WAM(X) of the Warren Abstract Machine and a corresponding generic compilation scheme of CLP(X) programs to WAM(X) code. The scheme is based on the specification and correctness proof for compilation of Prolog programs on the WAM in [32].

2

C. Beierle and E. Börger. A WAM extension for type-constraint logic programming: Specification and correctness proof. Research report IWBS 200, IBM Germany Science Center, Heidelberg, December 1991.

Contains the extension of [3] to the full Protos Abstract Machine by refining the abstract type constraints to the polymorphic order-sorted types of PROTOS-L.

3

C. Beierle and E. Börger. Correctness proof for the WAM with types. In E. Börger, G. Jäger, H. Kleine Büning, and M. M. Richter, editors, Computer Science Logic, volume 626 of Lecture Notes in Computer Science, pages 15-34. Springer, 1992. = Research Report IWBS 205, pp. ii+23, IBM Germany Science Center, Heidelberg, January 1992.

The Börger-Rosenzweig's specification and correctness proof for compiling Prolog to WAM [32] is extended to the Protos-L language which extends Prolog with polymorphic (dynamic) types. In this paper the type notion is kept abstract (as constraint) in order to allow application to different constraint formalisms. [2] extends the specification and the correctness proof to the full Protos Abstract Machine by refining the abstract type constraints to the polymorphic order-sorted types of PROTOS-L.

4

B. Blakley. A Smalltalk Evolving Algebra And Its Uses. PhD thesis, University of Michigan, Ann Arbor MI, 1992.

An early student work on evolving algebras (the late date of 1992 is accidental). A reduced version of Smalltalk is formalized and studied.

5

A. Blass and Y. Gurevich. Evolving Algebras and Linear Time Hierarchy. Extended Abstract. In B. Pehrson and I. Simon (Eds.) IFIP 13th World Computer Congress 1994, Volume I: Technology/Foundations, Elsevier, Amsterdam, 383-390.

There exists a sequential evolving algebra U (an allusion to ``universal'') and a constant c such that, under honest time counting, U simulates every other sequential evolving algebra in lock-step with lag factor c . In STOC'92, Neil Jones exhibited simple computation models where the time-speed-up theorem fails and linear time computable functions form a hierarchy. Jones' notion of linear time is too restrictive. To overcome that obstacle, we generalize the linear hierarchy theorem to sequential evolving algebras.

6

E. Börger. A logical operational semantics for full Prolog. Part I: Selection core and control. In E. Börger, H. Kleine Büning, M. M. Richter, and W. Schönfeld, editors, CSL'89. 3rd Workshop on Computer Science Logic, Lecture Notes in Computer Science, volume 440, pp. 36-64. Springer, 1990. = IBM Germany Science Center Heidelberg, IWBS Report 111, March 1990. Reprinted in: Proceedings The 3rd Logic Programming Winter School and Seminar. LOP'91, Ruprechtov, Czechoslovakia, pp. 65-94.

See comments to [8]

7

E. Börger. A logical operational semantics for full Prolog. Part II: Built-in predicates for database manipulations. In B. Rovan, editor, Mathematical Foundations of Computer Science, volume 452 of Lecture Notes in Computer Science, pages 1-14. Springer, 1990. = IBM Germany Science Center Heidelberg, IWBS Report 115, April 1990.

See comments to [8]

8

E. Börger. A logical operational semantics for full Prolog. Part III: Built-in predicates for files, terms, arithmetic and input-output. In Y. Moschovakis, editor, Logic from Computer Science, Berkeley Mathematical Sciences Research Institute Publications, volume 21, pp. 17-50. Springer, 1992. Preliminary version: IBM Germany Science Center Heidelberg, IWBS Report 117, April 1990.

These are the original 3 papers of Börger where he gives a complete evolving-algebra formalization of Prolog with all features discussed in the international Prolog standardization working group (WG17 of ISO/IEC JTC1 SC22), see [10]. The specification is developed by stepwise refinement, describing orthogonal language features by modular rule sets. An improved (tree instead of stack based) version is found in [30][27]; the revised final version is in [33].

9

E. Börger. Logic Programming: The Evolving Algebra Approach. In B. Pehrson and I. Simon (Eds.) IFIP 13th World Computer Congress 1994, Volume I: Technology/Foundations, Elsevier, Amsterdam, 391-395.

The paper surveys the work which has been done from 1986-1994 on specifications of logic programming systems by evolving algebras.

10

E. Börger and K. Dässler. Prolog: DIN papers for discussion. ISO/IEC JTCI SC22 WG17 Prolog standardization document no. 58, National Physical Laboratory, Middlesex, April 1990.

A version of [8][7][6] proposed to the international Prolog standardization committee as a complete formal semantics of Prolog. An improved version is in [33].

11

E. Börger, G. Del Castillo, P. Glavan, and D. Rosenzweig. Towards a mathematical specification of the APE100 architecture: the APESE model. In B. Pehrson and I. Simon (Eds.) IFIP 13th World Computer Congress 1994, Volume I: Technology/Foundations, Elsevier, Amsterdam,396-401.

Defines a lock-step parallel evolving algebra which models the high level programming view of the APE100 parallel architecture.

12

E. Börger and B. Demoen. A framework to specify database update views for Prolog. In M. J. Maluszynski, editor, PLILP'91. Third International Symposium on Programming Languages Implementation and Logic Programming, volume 528 of Lecture Notes in Computer Science, pages 147-158. Springer, 1991. Preliminary version: The view on database updates in Standard Prolog: a proposal and a rationale in: ISO/IEC JTC1 SC22 WG17 Prolog Standardization Report no. 74, February 1991, pp. 3-10.

Provides a precise definition of the major Prolog database update views (immediate, logical, minimal, maximal), within a framework closely related to [8][7][6].

13

E. Börger, I. Durdanovic, and D. Rosenzweig. Occam: Specification and compiler correctness. Part I: Simple mathematical interpreters. In U. Montanari, E.-R. Olderog (Eds.), Proc. PROCOMET'94 (IFIP Working Conference on Programming Concepts, Methods and Calculi), pages 489-508, North-Holland, 1994

A truly concurrent evolving algebra model of Occam is defined as basis for a provably correct, smooth transition to the Transputer Instruction Set architecture. This model is stepwise refined, in a provably correct way, providing: (a) an asynchronous implementation of synchronous channel communication, (b) its optimization for internal channels, (c) the sequential implementation of processors using priority and time-slicing.

14

E. Börger and U.Glässer. A formal specification of the PVM architecture. In B. Pehrson and I. Simon (Eds.) IFIP 13th World Computer Congress 1994, Volume I: Technology/Foundations, Elsevier, Amsterdam, 402-409.

Provides an evolving algebra model for the Parallel Virtual machine (PVM, the Oak Ridge National Laboratory software system that serves as general purpose environment for heterogeneous distributed computing). The model defines PVM at the C-interface, at the level of abstraction which is tailored to the programmer's understanding. Cf. the survey An abstract model of the parallel virtual machine (PVM) presented at 7th International Conference on Parallel and Distributed Computing Systems (PDCS'94), Las Vegas/Nevada, 5.-9.10.1994.

15

E. Börger, U. Glässer, and W. Müller. The semantics of Behavioral VHDL'92 Descriptions. In: EURO-DAC'94. European Design Automation Conference with EURO-VHDL'94. Proceedings IEEE CS Press, Los Alamitos, CA, 1994, pp.500-505.

Provides a transparent but precise evolving algebra definition of the signal behavior and time model of full elaborated VHDL'92. This includes guarded signals, delta and time delays, the two main propagation delay modes transport,inertial, and the three process suspensions (wait on/until/for). Shared variables, postponed processes and rejection pulse are covered.

16

E. Börger, U. Glässer, and W. Müller. Formal definition of an abstract VHDL'93 simulator by EA-machines. In C. Delgado Kloos and P. T. Breuer (Eds.), Formal Semantics for VHDL, Kluwer Academic Publishers, 1995.

Extends the work in [15] by including the treatment of variable assignments and of value propagation by ports.

17

E. Börger, Y. Gurevich, and D. Rosenzweig. The bakery algorithm: Yet another specification and verification. In E. Börger, editor, Specification and Validation Methods. Oxford University Press, 1994.

One evolving algebra A1 is constructed to reflect faithfully the algorithm. Then a more abstract evolving algebra A2 is constructed. It is checked that A2 is safe and fair, and that A1 correctly implements A2. The proofs work for atomic as well as, mutatis mutandis, for durative actions.

18

E. Börger, F. J. López-Fraguas, and M. Rodríguez-Artalejo. Towards a mathematical specification of a narrowing machine. Research report DIA 94/5, pp. I+30, Dep. Informática y Automática, Universidad Complutense, Madrid, March 1994.

Full version of [19], containing optimizations and proofs.

19

E. Börger, F. J. López-Fraguas, and M. Rodríguez-Artalejo. A model for mathematical analysis of functional logic programs and their implementations. In B. Pehrson and I. Simon (Eds.) IFIP 13th World Computer Congress 1994, Volume I: Technology/Foundations, Elsevier, Amsterdam, 410-415.

Defines an evolving algebra model for the innermost version of the functional logic programming language BABEL, extending the Prolog model of [33][30] by rules which describe the reduction of expressions to normal form. The model is stepwise refined towards a mathematical specification of the implementation of Babel by a graph-narrowing machine. The refinements are proved to be correct.

20

E. Börger and E. Riccobene. Logical operational semantics of Parlog. Part I: And-parallelism. In H. Boley and M. M. Richter, editors, Processing Declarative Knowledge, volume 567 of Lecture Notes in Artificial Intelligence, pages 191-198. Springer, 1991.

See comment to [23].

21

E. Börger and E. Riccobene. Logical operational semantics of Parlog. Part II: Or-parallelism. In A.Voronkov, editor, Logic Programming, volume 592 of Lecture Notes in Artificial Intelligence, pages 27-34. Springer, 1992.

See comment to [23].

22

E. Börger and E. Riccobene. A mathematical model of Concurrent Prolog. Research report CSTR-92-15, Dept. of Computer Science, University of Bristol, Bristol, 1992.

An evolving algebra formalization of Ehud Shapiro's Concurrent Prolog. Adaptation of the model defined for PARLOG in [23].

23

E. Börger and E. Riccobene. A formal specification of Parlog. In M. Droste and Y. Gurevich, editors, Semantics of Programming Languages and Model Theory, pages 1-42. Gordon and Breach, 1993. = TR 1/93, Dipartimento di Informatica, Università di Pisa, 1993.

An evolving algebra formalization of Parlog, a well known parallel version of Prolog. This formalization separates explicitly the two kinds of parallelism occurring in Parlog: AND-parallelism and OR-parallelism. It uses an implementation independent, abstract notion of terms and substitutions. Improved and extended version of [21][20], obtained combining the concurrent features of the Occam model of [52] with the logic programming model of [33][30].

24

E. Börger and E. Riccobene. Logic + control revisited: an abstract interpreter for Gödel programs. In G. Levi, editor, Advances in Logic Programming Theory. Oxford University Press, 1994.

Develops a simple evolving algebra interpreter for Gödel programs. This interpreter abstracts from the deterministic and sequential execution strategies of Prolog [32] and thus provides a precise interface between logic and control components for execution of Gödel programs. The construction is given in abstract terms which cover the general logic programming paradigm and allow for concurrency.

25

E. Börger and D. Rosenzweig. An analysis of Prolog database views and their uniform implementation. Research report CSE-TR-89-91, EECS, University of Michigan, Ann Arbor MI, 1991. Also issued by the international Prolog standardization committee as ISO/IEC JTCI SC22 WG17 document No. 80, National Physical Laboratory, Teddington 1991, pages 87-130.

A mathematical analysis of the Prolog database views defined in [12]. The analysis is derived by stepwise refinement of the stack model for Prolog from [29]. It leads to the proposal of a uniform implementation of the different views which discloses the tradeoffs between semantic clarity and efficiency of database update view implementations.

26

E. Börger and D. Rosenzweig. From Prolog algebras towards WAM-a mathematical study of implementation. In E. Börger, H. Kleine Büning, M. M. Richter, and W. Schönfeld, editors, CSL'90, 4th Workshop on Computer Science Logic, volume 533 of Lecture Notes in Computer Science, pages 31-66. Springer, 1991.

Refines Börger's Prolog model [7] by elaborating the conjunctive component-as reflected by compilation of clause structure into WAM code-and the disjunctive component-as reflected by compilation of predicate structure into WAM code. The correctness proofs for these refinements include last call optimization, determinacy detection and virtual copying of dynamic code. Improved in [29].

27

E. Börger and D. Rosenzweig. A formal specification of Prolog by tree algebras. In V. Ceric, V. Dobric, V. Luzar, and R. Paul, editors, Information Technology Interfaces, pages 513-518, Zagreb, 1991. University Computing Centre. Cf. abstract A natural formalization of full Prolog. In: Newsletter of the Association for Logic Programming, Short Communications, vol. 5/1, February 1992, pp. 8-9.

Prompted by discussion in the international Prolog standardization committee (ISO/IEC JTC1 SC22 WG17), this paper suggests to replace the stack based model of [6] and the stack implementation of the tree based model of [7] by a pure tree model for Prolog. An improved version of the latter is the basis for [33][30] where also an error in the treatment of the catch built-in predicate is corrected.

28

E. Börger and D. Rosenzweig. WAM algebras-a mathematical study of implementation, part 2. In A.Voronkov, editor, Logic Programming, volume 592 of Lecture Notes in Artificial Intelligence, pages 35-54. Springer, 1992. Preliminary version: Technical Report CSE-TR-88-91, Computer Science and Engineering Division, Department of Electrical Engineering and Computer Science, University of Michigan/Ann Arbor, April 1991, pp. 21.

Refines the Prolog model of [26] by elaborating the WAM code for representation and unification of terms. The correctness proof for this refinement includes environment trimming, Warren's variable classification and switching instructions. Improved in [29].

29

E. Börger and D. Rosenzweig. The WAM - definition and compiler correctness. Research report TR-14/92, Dipartimento di Informatica, Università di Pisa, Pisa, 1992.

Substantial example of the successive refinement method in the area, improving the predecessors [28][26]. A hierarchy of evolving algebras provides a solid foundation for constructing provably correct compilers from Prolog to WAM. Various refinement steps take care of different distinctive features (``orthogonal components'' in the authors' metaphor) of WAM making the specification as well as the correctness proof modular and extendible; examples of such extensions are found in [67][34][3][2]. The revised final version is in [32].

30

E. Börger and D. Rosenzweig. A simple mathematical model for full Prolog. Research report TR-33/92, Dipartimento di Informatica, Università di Pisa, Pisa, October 1992.

An improved version of [27][7][6], taking into account the ISO Prolog standardization effort. For the revised final version see [33].

31

E. Börger and D. Rosenzweig. The mathematics of set predicates in Prolog. In G. Gottlob, A. Leitsch, and D. Mundici, editors, Computational Logic and Proof Theory, volume 713 of Lecture Notes in Computer Science, pages 1-13. Springer, 1993. Also issued as Prolog. Copenhagen papers 2, ISO/IEC JTC1 SC22 WG17 Standardization report no. 105, National Physical Laboratory, Middlesex, 1993, pp. 33-42.

Provides a logical (proof-theoretical) specification of the solution collecting predicates findall, bagof of Prolog. This abstract definition allows a logico-mathematical analysis, rationale and criticism of various proposals made for implementations of these predicates (in particular of setof) in current Prolog systems. Foundational companion to section 5, on solution collecting predicates, in [33].

32

E. Börger and D. Rosenzweig. The WAM - definition and compiler correctness. In L. C. Beierle and L. Plümer, editors, Logic Programming: Formal Methods and Practical Applications, Series in Computer Science and Artificial Intelligence. North-Holland, 1994.

Revised and final version of [29].

33

E. Börger and D. Rosenzweig. A mathematical definition of full Prolog. In Science of Computer Programming, 1994. See the abstract Full Prolog in a Nutshell. In: Logic Programming (Proceedings of the 10th International Conference on Logic Programming) (D. S. Warren, Ed.), MIT Press 1993, p. 832.

An abstract evolving algebra specification of the semantics of Prolog, rigorously defining the international ISO Prolog standard (draft proposal) by stepwise refinement. Revised and final version of [30][27][7][6].

34

E. Börger and R. Salamone. CLAM specification for provably correct compilation of CLP(R ) programs. In E. Börger, editor, Specification and Validation Methods. Oxford University Press, 1994.

Extends the Börger-Rosenzweig's specification and correctness proof, for compiling Prolog programs to the WAM [32], to CLP(R) and the constraint logical arithmetical machine (CLAM) developed at IBM Yorktown Heights. Full proofs appear in [67].

35

E. Börger and P. Schmitt. A formal operational semantics for languages of type Prolog III. In E. Börger, H. Kleine Büning, M. M. Richter, and W. Schönfeld, editors, CSL'90, 4th Workshop on Computer Science Logic, volume 533 of Lecture Notes in Computer Science, pages 67-79. Springer, 1991. Preliminary version: IBM Germany, IWBS Report 144, November 1990, pp. 1-27.

An evolving algebra formalization of Alain Colmerauer's constraint logic programming language Prolog III, obtained from the Prolog model in [8][7][6] through extending unifications by constraint systems. This extension was the starting point for the extension of [32] in [3].

36

P. Glavan. Semanticka analiza istodobnih logickih programskih jezika (Semantical analysis of concurrent logic languages). Master's thesis (in Croation), University of Zagreb, Zagreb, 1993.

See comments for [37].

37

P. Glavan and D. Rosenzweig. Communicating evolving algebras. In E. Börger, H. Kleine Büning, G. Jäger, S. Martini, and M. M. Richter, editors, Computer Science Logic, Lecture Notes in Computer Science 702, pages 182-215. Springer, 1993.

A theory of concurrent computation within the framework of evolving algebras is developed, generalizing [22][21][20][52]. The power of the framework is demonstrated by modelling the Chemical Abstract Machine of Berry and Boudol and the -calculus of Milner.

38

P. Glavan and D. Rosenzweig. Evolving Algebra Model of Programming Language Semantics. In B. Pehrson and I. Simon (Eds.) IFIP 13th World Computer Congress 1994, Volume I: Technology/Foundations, Elsevier, Amsterdam, pp.416-422.

Evolving algebra interpretation of many-step SOS, denotational semantics and Hoare logic for the language of while-programs, together with correctness and completeness theorems, based on a simple flowchart model of the language.

39

G. Gottlob, G. Kappel, and M. Schrefl. Semantics of object-oriented data models - the evolving algebra approach. In J. W. Schmidt and A. A. Stogny, editors, Next Generation Information Technology, volume 504 of Lecture Notes in Computer Science, pages 144-160. Springer, 1991.

Uses evolving algebras to define the operational semantics of object creation, of overriding and dynamic binding, and of inheritance at the type level (type specialization) and at the instance level (object specialization).

40

Y. Gurevich. Logic and the challenge of computer science. In E. Börger, editor, Current Trends in Theoretical Computer Science, pages 1-57. Computer Science Press, 1988.

The introduction and the first use of evolving algebras (at the end of the paper).

41

Y. Gurevich. Algorithms in the world of bounded resources. In R. Herken, editor, The universal Turing machine - a half-century story, pages 407-416. Oxford University Press, 1988.

Early complexity theoretical motivation for introduction of evolving algebras is discussed.

42

Y. Gurevich. Evolving algebras. A tutorial introduction. Bulletin of EATCS, 43: 264-284, 1991. Slightly revised reprinted in Current Trends in Theoretical Computer Science, Eds. G. Rozenberg and A. Salomaa, World Scientific, 1993, 266-292.

The first tutorial on evolving algebras. The EA thesis is stated: Every algorithm can be simulated by an appropriate evolving algebra in lock-step on the natural abstraction level of the algorithm.

43

Y. Gurevich. Logic Activities in Europe. ACM SIGACT NEWS, 1994, to appear.

A critical analysis of European logic activities in computer science. The part relevant to evolving algebras is subsection 4.6 called Mathematics and Pedantics.

44

Y. Gurevich. Evolving Algebras 1993: Lipari Guide. Specification and Validation Methods, Ed. E. Börger, Oxford University Press, 1994.

The tutorial [42] covered basic evolving algebras. In the meantime, evolving algebras have been extensively used, in particular, for specifying parallel, distributed computations and computations involving real time. It became obvious that a more advanced definition of evolving algebras is needed. The guide addresses this need.

45

Y. Gurevich. Evolving Algebras. In B. Pehrson and I. Simon (Eds.) IFIP 13th World Computer Congress 1994, Volume I: Technology/Foundations, Elsevier, Amsterdam, 423-427.

The opening talk at the first EA workshop. Sections: Introduction, The EA Thesis, Remarks, Future Work.

46

Y. Gurevich and E. Grädel. Towards a Model Theory of Metafinite Structures. Logic Colloquium 1994.

Seemingly finite objects, like databases or states of algorithms, often have an infinite structure (e.g. arithmetic) somewhere in the background. (The phenomenon is known to evolving algebra practitioners.) A more careful formalizations of such finite objects should reflect the relevant infinite structure in one way or another. The problem is explained and some frameworks of carefully controlled infinity are proposed. The full paper is in preparation.

47

Y. Gurevich and J. Huggins. The semantics of the C programming language. In E. Börger, H. Kleine Büning, G. Jäger, S. Martini, and M. M. Richter, editors, Computer Science Logic, Lecture Notes in Computer Science 702, pages 274-309. Springer, 1993.

The method of successive refinements is used to give a succint semantics of the C programming language. See [48].

48

Y. Gurevich and J. Huggins. ERRATA to ``The Semantics of the C Programming Language''. In E. Börger, Y. Gurevich, K. Meinke, editors, Computer Science Logic, Lecture Notes in Computer Science 832, pages 334-336, Springer, 1994.

A correction of minor errors and omissions in [47].

49

Y. Gurevich and J. Huggins. Evolving Algebras and Partial Evaluation. In B. Pehrson and I. Simon (Eds.) IFIP 13th World Computer Congress 1994, Volume I: Technology/Foundations, Elsevier, Amsterdam, 587-592.

The paper describes an automated partial evaluator for sequential evolving algebras implemented at the University of Michigan.

50

Y. Gurevich and R. Mani. Group Membership Protocol: Specification and Verification. In Specification and Validation Methods, Ed. E. Börger, Oxford University Press, 1994.

An interesting and useful protocol of Flavio Christian involves timing constraints and its correctness is not obvious. The protocol is formally specified and verified. (The verification proof allowed the authors to simplify the assumptions slightly.)

51

Y. Gurevich and J. Morris. Algebraic operational semantics and Modula-2. In E. Börger, H. Kleine Büning, and M. M. Richter, editors, CSL'87, 1st Workshop on Computer Science Logic, volume 329 of Lecture Notes in Computer Science, pages 81-101. Springer, 1988.

An extended abstract of [58].

52

Y. Gurevich and L. Moss. Algebraic operational semantics and Occam. In E. Börger, H. Kleine Büning, and M. M. Richter, editors, CSL'89, 3rd Workshop on Computer Science Logic, volume 440 of Lecture Notes in Computer Science, pages 176-192. Springer, 1990.

The first application of evolving algebras to distributed parallel computing with the challenge of true concurrency.

53

J. Huggins. Kermit: Specification and Verification. In Specification and Validation Methods, Ed. E. Börger, Oxford University Press, 1994.

The Kermit file-transfer protocol (including a sliding windows extension to the basic protocol) is specified and verified using evolving algebras at several different layers of abstraction.

54

D. E. Johnson and L. S. Moss. Grammar Formalisms Viewed as Evolving Algebras. submitted to the Proceedings of the Third Meeting on Mathematics of Language, 1994.

Distributed Evolving Algebras are used to model formalisms for natural language syntax. The authors start by defining an evolving algebra model of context free derivations which abstracts from the parse tree descriptions used in [23][52] and from the dynamic tree generation appearing in [33][30][27]. Then the simple model of context free rules is extended to characterise in a uniform and natural way different context sensitive languages in terms of evolving algebras.

55

A. M. Kappel. Algebraische operationale Semantik und ihre Anwendungen auf Prolog. Master's thesis (in German), Universität Dortmund, Dortmund, 1990.

See [56].

56

A. M. Kappel. Executable Specifications based on Dynamic Algebras. In A. Voronkov, editor, Logic Programming and Automated Reasoning, volume 698 of LNAI, pages 229-240. Springer, 1993.

Defines a language for specification of evolving algebras and designs an abstract target machine (namely a Prolog program) which is specially tailored for executing evolving algebra computations. A prototype of the compiler has been implemented in Prolog. An extended abstract of [55].

57

R. Mani. The evolving algebra static semantics of SML. Preliminary version, 1992.

An evolving algebra description for the static semantics of Core ML. Preliminary version: a revised version is in preparation.

58

J. Morris. Algebraic operational semantics for Modula 2. PhD thesis, University of Michigan, Ann Arbor MI, 1988.

The earliest formalization of a real-life language. The semantical description is parse tree directed. In the meantime, the methodology has developed enabling more elegant descriptions, but one has to start somewhere. Abstract in [51].

59

J. Morris and G. Pottinger. Ada-Ariel semantics. Odyssey Research Associates, Inc., 80 pages, July 1990.

60

B. Müller. A Semantics for Hybrid Object-Oriented Prolog Systems. In B. Pehrson and I. Simon (Eds.) IFIP 13th World Computer Congress 1994, Volume I: Technology/Foundations, Elsevier, Amsterdam.

Extends the rules given in [33] for the user-defined core of Prolog to define the semantics of a hybrid object-oriented Prolog system. The definition covers the central object-oriented features of: object creation and deletion, data encapsulation, inheritance, messages, polymorphism and dynamic binding.

61

A. Poetzsch-Heffter. Interprocedural data flow analysis based on temporal specifications. Technical Report 93-1397, Cornell University, 1993.

Investigates the specification of data flow problems by temporal logic formulas and proves fixpoint analyses correct. Temporal formulas are interpreted w.r.t. programming language semantics given in the framework of evolving algebras.

62

A. Poetzsch-Heffter. Developing efficient interpreters based on formal language specifications. In P. Fritzson, editor, Compiler Construction, 1994. LNCS 786.

Reports on extensions of the MAX system enabling the generation and refinement of interpreters based on formal language specifications. In these specifications, static semantics is defined by an attribution mechanism and dynamic semantics is defined by evolving algebras.

63

A. Poetzsch-Heffter. Comparing action semantics and evolving algebra based specifications with respect to applications. In Proceedings of the First International Workshop on Action Semantics, 1994. Appears as technical report of the Aarhus University, Denmark.

Action semantics is compared to evolving algebra based language specifications. In particular, different aspects relevant to language documentation and programming tool development are discussed.

64

A. Poetzsch-Heffter. Deriving Partial Correctness Logics From Evolving Algebras. In B. Pehrson and I. Simon (Eds.) IFIP 13th World Computer Congress 1994, Volume I: Technology/Foundations, Elsevier, Amsterdam, 434-439.

A proposal for deriving partial correctness logics from simple evolving algebra models of programming languages. A basic axiom (schema) is derived from an evolving algebra and is used to obtain more convenient logics.

65

E. Riccobene. Modelli matematici per linguaggi logici (Mathematical models for logic languages). PhD thesis (in Italian), University of Catania, 1992.

Systematic treatment of evolving algebra models for Gödel [24], Parlog [23], Concurrent Prolog [22], GHC, Pandora.

66

D. Rosenzweig. Distributed Computations: Evolving Algebra Approach. In B. Pehrson and I. Simon (Eds.) IFIP 13th World Computer Congress 1994, Volume I: Technology/Foundations, Elsevier, Amsterdam, 440-441.

Remarks on some evolving algebra models of concurrent and parallel computation.

67

R. Salamone. Una specifica astratta e modulare della CLAM (An abstract and modular specification of the CLAM). Master's thesis (in Italian), Università di Pisa, Pisa, 1993.

Full version of [34].

68

J. Sauer. Wissensbasierte Lösen von Ablaufsplanungsproblemen durch explizite Heuristiken. PhD thesis, 1993. In: Dissertationen zur Künstlichen Intelligenz, Infix-Verlag, Dr. Ekkehardt Hundt, St. Augustin 1993, pp. 204.

Uses evolving algebras to define the semantics for selection and elaboration of heuristics for computation of goal sets in the language HERA.

69

M. Schrefl and G. Kappel. Cooperation contracts. In T. J. Teorey, editor, Proc. 10th International Conference on the Entity Relationship Approach, pages 285-307. E/R Institute, 1991.

The authors introduce the concept of cooperative message handling and use evolving algebras to give formal semantics.

70

M. Vale. The Evolving Algebra Semantics of COBOL. Part 1: Programs and Control. Research report CSE-TR-162-93, EECS, University of Michigan, Ann Arbor MI, 1993.

71

C. Wallace. The semantics of the C++ Programming Language. In E. Börger, editor, Specification and Validation Methods. Oxford University Press, 1994.

The semantical description in [47] is extended to encompass all of C++.

• About this document ...