Evolving Algebras 1993: Lipari Guide[1]

Yuri Gurevich[2]

[1]To appear in Specification and Validation Methods, Ed. E. Börger, Oxford University Press, 1994.

[2]Partially supported by ONR grant N00014-91-J-1861 and NSF grant CCR-92-04742.

• Introduction
  • The Pragmatic Occam's Razor
  • Acknowledgment
• Static Algebras and Updates
  • Static Algebras: Motivation
  • Vocabularies
    • Logic Names
  • Definition of Static Algebras
    • Universes
  • Terms
    • Appropriate States and the Fun Notation
  • Locations and Updates
  • Update Sets and Families of Update Sets
    • Remark
  • Conservative Determinism vs. Local Nondeterminism
• Sequential Evolving Algebras
  • Basic Transition Rules
    • Update Instructions
      • Semantics
    • Two Rule Constructors
      • The Sequence Constructor
      • The Conditional Constructor
    • Guarded Multi-updates
      • Remark
  • Importing New Elements
    • Reserve
      • Reserve Proviso
    • Transition Rules: Syntax
      • The Import Constructor
    • Auxiliary Vocabularies
    • Transition Rules: Semantics
      • Discarding Elements from Universes
    • Importing Several Elements at a Time
  • Programs and Runs
    • Programs and Pure Runs
    • External Functions
      • Runs
      • Internal and External Locations
      • Irrelevant Values of External Functions
• Nondeterministic Sequential Ealgebras and Some Other Simple Extensions of the Basic Model
  • Basic Evolving Algebras with Choice
    • Syntax
      • Choose Constructor
    • Semantics
      • Global Choice Semantics
      • Semantics without Global Choice
      • Remark
      • Runs
    • Abbreviations
  • Some Other Simple Extensions of the Basic Model
    • First-order Guards
      • Semantics
      • Remark
    • Qualified Choose Construct
      • Qualified Choose Constructor
    • Duplication
      • Semantics
• Parallelism: Evolving Algebras with Variables
  • Variables
  • Terms and Guards
  • A Parallel Version of the Basic EA Model
    • Syntax
      • The Declaration Constructor
      • Programs
    • Semantics of Rules
      • Remark
  • Importing Elements
    • Remark
  • Runs
• Distributed Evolving Algebras
  • The Self Function
  • Basic Definition of Distributed Ealgebras
    • Cooperative Actions
  • Generalizations
    • Active Agents
    • Active Teams
  • Sequential Runs
    • Stages
    • Quasi-sequential Runs
  • Partially Ordered Runs
    • Runs
  • Real-time Computations
• Bibliography
• About this document ...