Preface |
Overview |
"UML"-ising Formal Techniques |
The RAISE Specification Language: RSL |
Acknowledgments |
Brief Guide to Volume 2 |
Opening / Part I: |
Introduction / 1: |
Why This Volume? / 1.1: |
Why Master These Principles, Techniques and Tools? / 1.1.2: |
What Does This Volume "Contain"? / 1.1.3: |
How Does This Volume "Deliver"? / 1.1.4: |
Formal Techniques "Lite" / 1.2: |
An RSL Primer / 1.3: |
Types / 1.3.1: |
The RSL Predicate Calculus / 1.3.2: |
Concrete RSL Types / 1.3.3: |
[lambda]-Calculus+Functions / 1.3.4: |
Other Applicative Expressions / 1.3.5: |
Imperative Constructs / 1.3.6: |
Process Constructs / 1.3.7: |
Simple RSL Specifications / 1.3.8: |
Bibliographical Notes / 1.4: |
Specification Facets / Part II: |
Hierarchies and Compositions / 2: |
The Issues / 2.1: |
Informal Illustrations / 2.1.1: |
Formal Illustrations / 2.1.2: |
Initial Methodological Consequences / 2.2: |
Some Definitions / 2.2.1: |
Principles and Techniques / 2.2.2: |
The Main Example / 2.3: |
A Hierarchical, Narrative Presentation / 2.3.1: |
A Hierarchical, Formal Presentation / 2.3.2: |
A Compositional, Narrative Presentation / 2.3.3: |
A Compositional, Formal Presentation / 2.3.4: |
Discussion / 2.4: |
Bibliographical Notes: Stanislaw Leshniewski / 2.5: |
Exercises / 2.6: |
Denotations and Computations / 3: |
Computations and Denotations / 3.1: |
Syntax and Semantics / 3.1.2: |
Characterisations / 3.1.3: |
Denotational Semantics / 3.2: |
A Simple Example: Numerals / 3.2.1: |
The Denotational Principle / 3.2.2: |
Expression Denotations / 3.2.3: |
GOTO Continuations / 3.2.4: |
Discussion of Denotational Semantics / 3.2.5: |
Computational Semantics / 3.3: |
Two Examples / 3.3.1: |
Expression Computations / 3.3.3: |
Computational Semantics of GOTO Programs / 3.3.4: |
Computational Semantics of Coroutine Programs / 3.3.5: |
Review: Denotations and Computations / 3.3.6: |
Some Pioneers of Semantics / 3.5: |
John McCarthy / 3.5.1: |
Peter Landin / 3.5.2: |
Configurations: Contexts and States / 3.6: |
"Real-World" Contexts and States / 4.1: |
A Physical System: Context and State / 4.3.1: |
Configurations of Contexts and States / 4.3.2: |
Nonphysical System: Context and State / 4.3.3: |
Discussion, I / 4.3.4: |
Discussion, II / 4.3.5: |
First Summary: Contexts and States / 4.4: |
General / 4.4.1: |
Development Principles and Techniques / 4.4.2: |
Programming Language Configurations / 4.5: |
Concurrent Process Configurations / 4.6: |
The Example / 4.6.1: |
Summary / 4.6.2: |
Second Summary: Contexts and States / 4.7: |
Information States and Behaviour States / 4.8: |
Program Flowcharts as State Machine Data / 4.8.1: |
Flowcharts [identical with] Machines / 4.8.2: |
Flowchart Machines / 4.8.3: |
Observations / 4.8.4: |
Conclusion / 4.8.5: |
Final Summary: Contexts and States / 4.9: |
A Crucial Domain and Computing Facet / 4.10: |
Time, Space and Space/Time / 5: |
Time / 5.1: |
Time - The Basics / 5.1.1: |
Time - General Issues / 5.1.2: |
"A-Series" and "B-Series" Models of Time / 5.1.3: |
A Continuum Theory of Time / 5.1.4: |
Temporal Events / 5.1.5: |
Temporal Behaviour / 5.1.6: |
Representation of Time / 5.1.7: |
Operations "on" Time / 5.1.8: |
Space / 5.2: |
Space - The Basics / 5.2.1: |
Location-Varying Entities / 5.2.2: |
Locations and Dynamicity / 5.2.3: |
Space - General Issues / 5.2.4: |
Space/Time / 5.3: |
A Guiding Example / 5.3.1: |
Representation of Space/Time / 5.3.2: |
Blizard's Theory of Time-Space / 5.3.3: |
Linguistics / 5.4: |
Pragmatics / 6: |
Everyday Pragmatics / 6.1: |
"Formal" Pragmatics / 6.3: |
Bibliographical Note / 6.4: |
Semantics / 6.6: |
Concrete Semantics / 7.1: |
"Abstract" Semantics / 7.3: |
Preliminary Semantics Concepts / 7.4: |
Syntactic and Semantic Types / 7.4.1: |
Contexts / 7.4.2: |
States / 7.4.3: |
Configurations / 7.4.4: |
Interpretation, Evaluation and Elaboration / 7.4.5: |
Simple Case / 7.5: |
Composite Case / 7.5.2: |
Macro-expansion Semantics / 7.6: |
Rewriting / 7.6.1: |
Macro-expansion / 7.6.2: |
Inductive Rewritings / 7.6.3: |
Fix Point Evaluation / 7.6.4: |
Operational and Computational Semantics / 7.7: |
Stack Semantics / 7.7.1: |
Attribute Grammar Semantics / 7.7.2: |
Proof Rule Semantics / 7.8: |
Principles, Techniques and Tools / 7.9: |
Syntax / 7.10: |
Form and Content: Syntax and Semantics / 8.1: |
Structure and Contents of This Chapter / 8.1.2: |
Sentential Versus Semantical Structures / 8.2: |
Examples of Sentential Structures / 8.2.1: |
Examples of Semantical Structures / 8.2.3: |
The First Abstract Syntax, John McCarthy / 8.3: |
Analytic Grammars: Observers and Selectors / 8.3.1: |
Synthetic Grammars: Generators / 8.3.2: |
BNF Grammars [approximate] Concrete Syntax / 8.4: |
BNF Grammars / 8.4.1: |
BNF[left and right arrow]RSL Parse Trees Relations / 8.4.2: |
Structure Generators and Recognisers / 8.5: |
Context-Free Grammars and Languages / 8.5.1: |
Parse Trees / 8.5.2: |
Regular Expressions and Languages / 8.5.3: |
Language Recognisers / 8.5.4: |
XML: Extensible Markup Language / 8.6: |
An Example / 8.6.1: |
Historical Background / 8.6.2: |
The Current XML "Craze" / 8.6.4: |
XML Expressions / 8.6.5: |
XML Schemas / 8.6.6: |
References / 8.6.7: |
Abstract Syntaxes / 8.7: |
Abstract Syntax of a Storage Model / 8.7.1: |
Abstract Syntaxes of Other Storage Models / 8.7.2: |
Converting RSL Types to BNF / 8.8: |
The Problem / 8.8.1: |
A Possible Solution / 8.8.2: |
Discussion of Informal and Formal Syntax / 8.9: |
Semiotics / 8.9.1: |
Semiotics = Syntax [plus sign in circle] Semantics [plus sign in circle] Pragmatics / 9.1: |
Language Components / 9.2: |
Languages and Systems / 9.4: |
Professional Languages / 9.5.1: |
Metalanguages / 9.5.2: |
Systems / 9.5.3: |
System Diagram Languages / 9.5.4: |
Discussion of System Concepts / 9.5.5: |
Systems as Languages / 9.5.6: |
Charles Sanders Peirce / 9.6: |
Further Specification Techniques / 9.8: |
Modularisation / 10: |
Some Examples / 10.1: |
Preparatory Discussion / 10.1.2: |
Structure of Chapter / 10.1.3: |
RSL Classes, Objects and Schemes / 10.2: |
Introducing the RSL "class" Concept / 10.2.1: |
The RSL "class" Concept / 10.2.2: |
The RSL "object" Concept / 10.2.3: |
The RSL "scheme" Concept / 10.2.4: |
RSL "scheme" Parameterisation / 10.2.5: |
A "Large-Scale" Example / 10.2.6: |
Definitions: Class, Scheme and Object / 10.2.7: |
UML and RSL / 10.3: |
Overview of UML Diagrams / 10.3.1: |
Class Diagrams / 10.3.2: |
Example: Railway Nets / 10.3.3: |
Comparison of UML and RSL OO Constructs / 10.3.5: |
Class Diagram Limitations / 10.3.6: |
Modularity Issues / 10.4: |
Automata and Machines / 10.4.2: |
Discrete State Automata / 11.1: |
Intuition / 11.1.1: |
Motivation / 11.1.2: |
Discrete State Machines / 11.1.3: |
Finite State Automata / 11.3: |
Regular Expression Language Recognisers / 11.3.1: |
Regular Expressions / 11.3.2: |
Formal Languages and Automata / 11.3.3: |
Automaton Completion / 11.3.4: |
Nondeterministic Automata / 11.3.5: |
Minimal State Finite Automata / 11.3.6: |
Finite State Automata Formalisation, I / 11.3.7: |
Finite State Automata Realisation, I / 11.3.8: |
Finite State Automaton Formalisation, II / 11.3.9: |
Finite State Automata Realisation, II / 11.3.10: |
Finite State Automata - A Summary / 11.3.11: |
Finite State Machines / 11.4: |
Finite State Machine Controllers / 11.4.1: |
Finite State Machine Parsers / 11.4.2: |
Finite State Machine Formalisation / 11.4.3: |
Finite State Machine Realisation / 11.4.4: |
Finite State Machines - A Summary / 11.4.5: |
Pushdown Stack Devices / 11.5: |
Pushdown Stack Automata and Machines / 11.5.1: |
Formalisation of Pushdown Stack Machines / 11.5.2: |
Pushdown Stack Device Summary / 11.5.3: |
Bibliographical Notes: Automata and Machines / 11.6: |
Concurrency and Temporality / 11.7: |
Petri Nets / Christian Krog Madsen12: |
Condition Event Nets (CENs) / 12.1: |
Description / 12.2.1: |
Small CEN Examples / 12.2.2: |
An RSL Model of Condition Event Nets / 12.2.3: |
Place Transition Nets (PTNs) / 12.3: |
Small PTN Examples / 12.3.1: |
An RSL Model of Place Transition Nets / 12.3.3: |
Railway Domain Petri Net Examples / 12.3.4: |
Coloured Petri Nets (CPNs) / 12.4: |
A CPN Example / 12.4.1: |
An RSL Model of Coloured Petri Nets / 12.4.3: |
Timed Coloured Petri Nets / 12.4.4: |
CEN Example: Work Flow System / 12.5: |
Project Planning / 12.5.1: |
Project Activities / 12.5.2: |
Project Generation / 12.5.3: |
CPN and RSL Examples: Superscalar Processor / 12.6: |
Coloured Petri Net Model / 12.6.1: |
RSL Model: Superscalar Processor / 12.6.3: |
Message and Live Sequence Charts / 12.7: |
Message Sequence Charts / 13.1: |
Basic MSCs (BMSCs) / 13.1.1: |
High-Level MSCs (HMSCs) / 13.1.3: |
An RSL Model of HMSC Syntax / 13.1.4: |
MSCs Are HMSCs / 13.1.5: |
Syntactic Well-formedness of MSCs / 13.1.6: |
An Example: IEEE 802.11 Wireless Network / 13.1.7: |
Semantics of Basic Message Sequence Charts / 13.1.8: |
Semantics of High-Level Message Sequence Charts / 13.1.9: |
Live Sequence Charts: Informal Presentation / 13.2: |
Live Sequence Chart Syntax / 13.2.1: |
A Live Sequence Chart Example, I / 13.2.2: |
Process Algebra / 13.3: |
The Process Algebra PA[subscript epsilon] / 13.3.1: |
Semantics of PA[subscript epsilon] / 13.3.2: |
The Process Algebra PAc[subscript epsilon] / 13.3.3: |
Semantics for PAc[subscript epsilon] / 13.3.4: |
Algebraic Semantics of Live Sequence Charts / 13.4: |
Textual Syntax of Live Sequence Charts / 13.4.1: |
Semantics of Live Sequence Charts / 13.4.2: |
The Live Sequence Chart Example, II / 13.4.3: |
Relating Message Charts to RSL / 13.5: |
Types of Integration / 13.5.1: |
An RSL Subset / 13.5.2: |
Relating Live Sequence Charts to RSL / 13.5.3: |
Checking Satisfaction / 13.5.4: |
Tool Support / 13.5.5: |
Communicating Transaction Processes (CTP) / 13.6: |
Narration of CTPs / 13.6.1: |
A Dining Philosophers Example / 13.6.3: |
Formalisation of CTPs / 13.6.4: |
Statecharts / 13.7: |
A Narrative Description of Statecharts / 14.1: |
An RSL Model of the Syntax of Statecharts / 14.3: |
Examples / 14.4: |
Railway Line Automatic Blocking / 14.4.1: |
Railway Line Direction Agreement System / 14.4.2: |
Wireless Rain Gauge / 14.4.3: |
A Process Algebra for Statecharts / 14.5: |
SPL: The Statechart Process Language / 14.5.1: |
Semantics of SPL / 14.5.2: |
Equivalence for SPL Terms / 14.5.3: |
Semantics of Statecharts / 14.6: |
An SPL Semantics for Statecharts / 14.6.1: |
Statechart Example / 14.6.2: |
Relating Statecharts to RSL / 14.7: |
Syntactical Restrictions / 14.7.1: |
Satisfaction Relation / 14.7.2: |
Quantitative Models of Time / 14.7.3: |
Soft Temporalities / 15.1: |
Hard Temporalities / 15.1.2: |
Soft and Hard Real-Time / 15.1.3: |
Examples - "Ye Olde Way"! / 15.1.4: |
Structure of This Chapter / 15.1.5: |
Temporal Logic / 15.2: |
A Philosophical Linguistics Background / 15.2.1: |
Interval Temporal Logic, ITL / 15.2.3: |
The Classic Temporal Operators: [diamond], [square] / 15.2.4: |
The Duration Calculus / 15.3: |
Examples, Part I / 15.3.1: |
Some Basic Notions / 15.3.2: |
Examples, Part II / 15.3.3: |
The Syntax / 15.3.4: |
The Informal Semantics / 15.3.5: |
Examples, Part III / 15.3.6: |
Transitions and Events / 15.3.7: |
Discussion: From Domains to Designs / 15.3.8: |
TRSL: RSL with Timing / 15.4: |
TRSL Design Criteria / 15.4.1: |
The TRSL Language / 15.4.2: |
Another Gas Burner Example / 15.4.3: |
RSL with Timing and Durations / 15.4.4: |
Review of TRSL / 15.5.1: |
TRSL and Duration Calculus / 15.5.2: |
Interpreter and Compiler Definitions / 15.6: |
SAL: Simple Applicative Language / 16: |
A Caveat / 16.1: |
The SAL Syntax / 16.2: |
Informal Exposition of SAL Syntax / 16.2.1: |
Formal Exposition of SAL Syntax / 16.2.2: |
Comments / 16.2.3: |
A Denotational Semantics / 16.3: |
An Informal Semantics / 16.3.1: |
A Formal Semantics / 16.3.2: |
Review of SAL Semantics, 1 / 16.3.3: |
Two Asides / 16.3.4: |
A First-Order Applicative Semantics / 16.4: |
Syntactic Types / 16.4.1: |
Semantic Types / 16.4.2: |
Abstraction Functions / 16.4.3: |
Auxiliary Functions / 16.4.4: |
Semantic Functions / 16.4.5: |
Review / 16.4.6: |
Review of SAL Semantics, 2 / 16.4.7: |
An Abstract, Imperative Stack Semantics / 16.5: |
Design Decisions - Informal Motivation / 16.5.1: |
Semantics Style Observations / 16.5.2: |
Run-Time Functions / 16.5.3: |
Review of SAL Semantics, 3 / 16.5.7: |
A Macro-expansion Semantics / 16.6: |
Analysis of Stack Semantics / 16.6.1: |
Compile-Time Types / 16.6.2: |
Run-Time Semantic Types / 16.6.4: |
Run-Time State / 16.6.5: |
Run-Time Stack Operations / 16.6.6: |
Run-Time Stack Search for Variable Values / 16.6.7: |
Macro-expansion Functions / 16.6.8: |
Review of SAL Semantics, 4 / 16.6.9: |
ASM: An Assembler Language / 16.7: |
The Computer State / 16.7.1: |
The Address Concept / 16.7.3: |
Machine Instructions / 16.7.4: |
Machine Semantics / 16.7.5: |
Review of ASM / 16.7.6: |
A Compiling Algorithm / 16.8: |
Compile-Time Types and State / 16.8.1: |
Compile-Time Dynamic Function / 16.8.3: |
Compile-Time Static Function / 16.8.4: |
Run-Time Constant Values / 16.8.5: |
Compilation Functions / 16.8.6: |
Review of Compiling Algorithm / 16.8.7: |
An Attribute Grammar Semantics / 16.9: |
Abstract Syntactic Types / 16.9.1: |
SAL BNF Grammar, 1 / 16.9.2: |
Node Attributes / 16.9.3: |
Constants / 16.9.4: |
Some Typographical Distinctions / 16.9.5: |
Review of Attribute Semantics, 1 / 16.9.6: |
Another Attribute Grammar Semantics / 16.10: |
SAL BNF Grammar, 2 / 16.10.1: |
Global Variables / 16.10.3: |
Review of Attribute Semantics, 2 / 16.10.4: |
Review and Bibliographical Notes / 16.11: |
SIL: Simple Imperative Language / 16.13: |
The Background / 17.1: |
Concrete, Schematic Syntax / 17.2: |
Abstract Syntax / 17.2.2: |
Imperative Denotational Semantics / 17.3: |
Auxiliary Semantic Functions / 17.3.1: |
Compile-Time Semantic Types / 17.3.3: |
Run-Time State Declaration and Initialisation / 17.4.3: |
Macros / 17.4.5: |
SMIL: Simple Modular, Imperative Language / 17.5: |
Compile/Run-Time Semantic Types / 18.1: |
SPIL: Simple Parallel, Imperative Language / 18.3.3: |
Informal Syntax / 19.1: |
Formal Syntax / 19.2.2: |
Process Concepts and Semantic Types / 19.3: |
Syntactic Notions / 19.3.1: |
Machines and Interpreters / 19.3.2: |
Semantic Notions and Types / 19.3.3: |
Process-Oriented Semantic Types / 19.4: |
Unique Process Identifiers [pi] : [Pi] / 19.4.1: |
The Heap [xi] : [Xi] / 19.4.2: |
Input/Output Channel Bindings / 19.4.3: |
Environments [rho] : ENV / 19.4.4: |
State Composition [Psi], [Gamma], [Xi], [Sigma], [Omega] / 19.4.5: |
Initial and Auxiliary Semantic Functions / 19.5: |
Start Function / 19.5.1: |
System Function / 19.5.2: |
Bind and Allocate Functions / 19.5.3: |
Free and Bound Functions / 19.5.4: |
Distribute Function / 19.5.5: |
Transition Loop / 19.5.6: |
The Next-State Transition Function / 19.6: |
The Assignment Statement / 19.6.2: |
The case Statement / 19.6.3: |
The while Loop / 19.6.4: |
The repeat until Loop / 19.6.5: |
Simple Input/Output Processes / 19.6.6: |
The Parallel Process Command, [double vertical line] / 19.6.7: |
The stop Process Technicality / 19.6.8: |
The Process call Command / 19.6.9: |
Internal Nondeterministic Processes, [characters not reproducible] / 19.6.10: |
External Nondeterministic Processes, [characters not reproducible] / 19.6.11: |
Nondeterministic Input/Output Processes / 19.6.12: |
The Embedded System Process Command / 19.6.13: |
A finish Process Technicality / 19.6.14: |
Closing / 19.7: |
A Summary / 20: |
Conclusion: Volumes 1 and 2 / 20.2: |
Preview of Volume 3 / 20.3: |
Appendixes / 20.4: |
Naming Convention / A: |
Indexes / B: |
Symbols Index / B.1: |
Time/Space / B.1.1: |
Modular RSL / B.1.2: |
Live Sequence Charts / B.1.3: |
Temporal Logics / B.1.6: |
Duration Calculus / B.1.8: |
Timed RSL: TRSL / B.1.9: |
Abbreviations / B.1.10: |
Concepts Index / B.2: |
Characteriations and Definitions Index / B.3: |
Authors Index / B.4: |