close
1.

電子ブック

EB
Andrea Corradini, Hartmut Ehrig, Takeo Kanade, Ugo Montanari, Leila Ribeiro, Grzegorz Rozenberg
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2006
所蔵情報: loading…
2.

電子ブック

EB
Dines Bj?rner, Wilfried Brauer, Grzegorz Rozenberg
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2006
所蔵情報: loading…
目次情報: 続きを見る
Preface
Reasons for Writing These Volumes
Shortcomings of These Volumes
Methods of Approach
A New Look at Software
Formal Techniques "Light"
The "Super Programmer"
What Is Software Engineering?
The Author's Aspirations
Role of These Volumes in an SE Education Programme
Why So Much Material?
How to Use These Volumes in a Course
Brief Guide to the Book
Guide to This Volume
Acknowledgments
Opening / Part I:
Introduction / 1:
Setting the Stage / 1.1:
A Software Engineering Triptych / 1.2:
Documentation / 1.3:
Formal Techniques and Formal Tools / 1.4:
Method and Methodology / 1.5:
The Very Bases of Software / 1.6:
Aims and Objectives / 1.7:
Bibliographical Notes / 1.8:
Exercises / 1.9:
Discrete Mathematics / Part II:
Numbers / 2:
Numerals and Numbers / 2.1:
Subsets of Numbers / 2.3:
Type Definitions: Numbers / 2.4:
Summary / 2.5:
Sets / 2.6:
Background / 3.1:
Mathematical Sets / 3.2:
Special Sets / 3.3:
Sorts and Type Definitions: Sets / 3.4:
Sets in RSL / 3.5:
Cartesians / 3.6:
The Issues / 4.1:
Cartesian-Valued Expressions / 4.2:
Cartesian Types / 4.3:
Cartesian Arity / 4.4:
Cartesian Equality / 4.5:
Some Construed Examples / 4.6:
Sorts and Type Definitions: Cartesians / 4.7:
Cartesians in RSL / 4.8:
Types / 4.9:
Values and Types / 5.1:
Phenomena and Concept Types / 5.2:
Programming Language Type Concepts / 5.3:
Sorts or Abstract Types / 5.4:
Built-in and Concrete Types / 5.5:
Type Checking / 5.6:
Types as Sets, Types as Lattices / 5.7:
Functions / 5.8:
General Overview / 6.1:
How Do Functions Come About? / 6.2:
An Aside: On the Concept of Evaluation / 6.4:
Function Algebras / 6.5:
Currying and [lambda]-Notation / 6.6:
Relations and Functions / 6.7:
Type Definitions / 6.8:
Conclusion / 6.9:
A [lambda]-Calculus / 6.10:
Informal Introduction / 7.1:
A "Pure" [lambda]-Calculus Syntax / 7.2:
A [lambda]-Calculus Pragmatics / 7.3:
A "Pure" [lambda]-Calculus Semantics / 7.4:
Call-by-Name Versus Call-by-Value / 7.5:
The Church-Rosser Theorems - Informal Version / 7.6:
The RSL [lambda]-Notation / 7.7:
Fix Points / 7.8:
Discussion / 7.9:
Algebras / 7.10:
Formal Definition of the Algebra Concept / 8.1:
How Do Algebras Come About? / 8.3:
Kinds of Algebras / 8.4:
Specification Algebras / 8.5:
RSL Syntax for Algebra Specifications / 8.6:
Mathematical Logic / 8.7:
Proof Theory Versus Model Theory / 9.1:
A Language of Boolean Ground Terms / 9.3:
Languages of Propositional Logic / 9.4:
Languages of Predicate Logic / 9.5:
Axiom Systems / 9.6:
Simple RSL / 9.7:
General
RSL Versus VDM-SL, Z and B
What, Syntactically, Constitutes a Specification?
Towards an RSL "Standard"
RSL Tools
Atomic Types and Values in RSL / 10:
The RSL Numbers / 10.1:
Enumerated Tokens / 10.3:
Characters and Texts / 10.4:
Identifiers and General Tokens / 10.5:
Function Definitions in RSL / 10.6:
The Function Type / 11.1:
Model-Oriented Explicit Definitions / 11.2:
Model-Oriented Axiomatic Definitions / 11.3:
Model-Oriented pre/post-Condition Definitions / 11.4:
Property-Oriented Axiomatic Definitions / 11.5:
Property-Oriented Algebraic Definitions / 11.6:
Summary of RSL Function Definition Styles / 11.7:
Property-Oriented and Model-Oriented Abstraction / 11.8:
Abstraction / 12.1:
Property-Oriented Abstractions / 12.2:
Model Versus Property Abstractions / 12.3:
Model-Oriented Abstractions / 12.4:
Principles, Techniques and Tools / 12.5:
Sets: The Issues / 12.6:
The Set Data Type / 13.2:
Examples of Set-Based Abstractions / 13.3:
Abstracting and Modelling With Sets / 13.4:
Inductive Set Definitions / 13.5:
A Comment on Varying Sets / 13.6:
Cartesians: The Issues / 13.7:
The Cartesian Data Type / 14.2:
Examples of Cartesian Abstractions / 14.3:
Abstracting and Modelling with Cartesians / 14.4:
Inductive Cartesian Definitions / 14.5:
Lists in RSL / 14.6:
Issues Related to Lists / 15.1:
The List Data Type / 15.2:
Small Examples of List-Based Abstractions / 15.3:
Abstracting and Modelling with Lists / 15.4:
Inductive List Definitions / 15.5:
A Review of List Abstractions and Models / 15.6:
Lists: A Discussion / 15.7:
Maps in RSL / 15.8:
The Map Data Type / 16.1:
Examples of Map-Based Abstractions / 16.3:
Abstracting and Modelling with Maps / 16.4:
Inductive Map Definitions / 16.5:
A Review of Map Abstractions and Models / 16.6:
Maps: A Discussion / 16.7:
Higher-Order Functions in RSL / 16.8:
Functions: The Issues / 17.1:
Examples Using Function-Based Abstractions / 17.2:
Abstracting and Modelling With Functions / 17.3:
Inductive Function Definitions / 17.4:
Review of Function Abstractions and Models / 17.5:
Specification Types / 17.6:
Types in RSL / 18:
Type Categories / 18.1:
Enumerated Token Types Revisited / 18.3:
Records: Constructors and Destructors / 18.4:
Union Type Definitions / 18.5:
Short Record Type Definitions / 18.6:
Type Expressions, Revisited / 18.7:
Subtypes / 18.8:
Type Definitions, Revisited / 18.9:
On Recursive Type Definitions / 18.10:
Specification Programming / 18.11:
On Specification Programming
On Problems and Exercises
Applicative Specification Programming / 19:
Scope and Binding / 19.1:
Intuition / 19.2:
Operator/Operand Expressions / 19.3:
Enumerated and Comprehended Expressions / 19.4:
Conditional Expressions / 19.5:
Bindings, Typings, Patterns and Matching / 19.6:
Review and Discussion / 19.7:
Imperative Specification Programming / 19.8:
Imperative Combinators: A [lambda]-Calculus / 20.1:
Variable References: Pointers / 20.3:
Function Definitions and Expressions / 20.4:
Translations: Applicative to Imperative / 20.5:
Styles of Configuration Modelling / 20.6:
Concurrent Specification Programming / 20.7:
Behaviour and Process Abstractions / 21.1:
Communicating Sequential Processes, CSP / 21.2:
The RSL/CSP Process Combinators / 21.4:
Translation Schemas / 21.5:
Parallelism and Concurrency: A Discussion / 21.6:
And So On! / 21.7:
Etcetera! / 22:
What Have We Covered? / 22.1:
What Is Next? / 22.2:
What Is Next-Next? / 22.3:
A Caveat / 22.4:
Formal Methods "Lite" / 22.5:
Appendixes / 22.6:
Common Exercise Topics / A:
Transportation Nets / A.1:
Container Logistics / A.2:
Financial Service Industry / A.3:
Summary References to Exercises / A.4:
Glossary / B:
Categories of Reference Lists / B.1:
Typography and Spelling / B.2:
The Glosses / B.3:
Indexes / C:
Symbols Index / C.1:
Concepts Index / C.2:
Characterisations and Definitions Index / C.3:
Authors Index / C.4:
References
Preface
Reasons for Writing These Volumes
Shortcomings of These Volumes
3.

電子ブック

EB
Dines Bj?rner, Dines Bj?rner, Grzegorz Rozenberg
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2006
所蔵情報: loading…
目次情報: 続きを見る
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:
Preface
Overview
"UML"-ising Formal Techniques
4.

電子ブック

EB
Wilfried Brauer, Hartmut Ehrig, Grzegorz Rozenberg
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2006
所蔵情報: loading…
目次情報: 続きを見る
Introduction to Graph Transformation Systems / Part I:
General Introduction / 1:
General Overview of Graph Grammars and Graph Transformation / 1.1:
What Is Graph Transformation? / 1.1.1:
Aims and Paradigms of Graph Transformation / 1.1.2:
Overview of Various Approaches / 1.1.3:
The Main Ideas of the Algebraic Graph Transformation Approach / 1.2:
The DPO Approach / 1.2.1:
The Algebraic Roots / 1.2.2:
From the DPO to the SPO Approach / 1.2.3:
From Graphs to High-Level Structures / 1.2.4:
The Chapters of This Book and the Main Results / 1.3:
Part I: Introduction to Graph Transformation Systems / 1.3.1:
Part II: Adhesive HLR Categories and Systems / 1.3.2:
Part III: Typed Attributed Graph Transformation Systems / 1.3.3:
Part IV: Case Study and Tool Support / 1.3.4:
Appendices / 1.3.5:
Hints for Reading This Book / 1.3.6:
Bibliographic Notes and Further Topics / 1.4:
Concepts of Graph Grammars and Graph Transformation Systems / 1.4.1:
Application Areas of Graph Transformation Systems / 1.4.2:
Languages and Tools for Graph Transformation Systems / 1.4.3:
Future Work / 1.4.4:
Graphs, Typed Graphs, and the Gluing Construction / 2:
Graphs and Typed Graphs / 2.1:
Introduction to Categories / 2.2:
Pushouts as a Gluing Construction / 2.3:
Pullbacks as the Dual Construction of Pushouts / 2.4:
Graph Transformation Systems / 3:
Basic Definitions for GT Systems / 3.1:
Construction of Graph Transformations / 3.2:
Local Church-Rosser and Parallelism Theorems for GT Systems / 3.3:
Overview of Some Other Main Results for GT Systems / 3.4:
Concurrency Theorem / 3.4.1:
Embedding and Extension Theorems / 3.4.2:
Confluence, Local Confluence, Termination, and Critical Pairs / 3.4.3:
Functional Behavior of GT Systems and Termination Analysis / 3.4.4:
Graph Constraints and Application Conditions / 3.5:
Adhesive High-Level Replacement Categories and Systems / Part II:
Adhesive High-Level Replacement Categories / 4:
Van Kampen Squares and Adhesive Categories / 4.1:
Adhesive HLR Categories / 4.2:
HLR Properties of Adhesive HLR Categories / 4.3:
Adhesive High-Level Replacement Systems / 5:
Basic Concepts of Adhesive HLR Systems / 5.1:
Instantiation of Adhesive HLR Systems / 5.2:
Graph and Typed Graph Transformation Systems / 5.2.1:
Hypergraph Transformation Systems / 5.2.2:
Petri Net Transformation Systems / 5.2.3:
Algebraic Specification Transformation Systems / 5.2.4:
Typed Attributed Graph Transformation Systems / 5.2.5:
The Local Church-Rosser and Parallelism Theorems / 5.3:
Concurrency Theorem and Pair Factorization / 5.4:
Embedding and Local Confluence / 6:
Initial Pushouts and the Gluing Condition / 6.1:
Critical Pairs / 6.2:
Local Confluence Theorem / 6.4:
Constraints and Application Conditions / 7:
Definition of Constraints and Application Conditions / 7.1:
Construction of Application Conditions from Constraints / 7.2:
Construction of Left from Right Application Conditions / 7.3:
Guaranteeing and Preservation of Constraints / 7.4:
Typed Attributed Graphs / Part III:
Attributed Graphs and Typing / 8.1:
Pushouts as a Gluing Construction of Attributed Graphs / 8.2:
Pullbacks of Attributed Graphs / 8.3:
Basic Concepts for Typed AGT Systems / 9:
Construction of Typed Attributed Graph Transformations / 9.2:
Local Church-Rosser and Parallelism Theorem for Typed AGT Systems / 9.3:
Concurrency Theorem and Pair Factorization for Typed AGT Systems / 9.4:
Pair Factorizations / 9.4.1:
Embedding and Local Confluence for Typed AGT Systems / 9.4.2:
Embedding and Extension Theorems for Typed AGT Systems / 10.1:
Critical Pairs for Typed AGT Systems / 10.2:
Local Confluence Theorem for Typed AGT Systems / 10.3:
Adhesive HLR Categories for Typed Attributed Graphs / 11:
Attributed Graph Structure Signatures and Typed Attributed Graphs / 11.1:
Definition of Concrete Adhesive HLR Categories / 11.2:
Verification of the Main Results for Typed AGT Systems / 11.3:
Constraints, Application Conditions and Termination for TAGT Systems / 12:
Constraints and Application Conditions for Typed AGT Systems / 12.1:
Equivalence of Constraints and Application Conditions / 12.2:
Termination Criteria for Layered Typed Attributed Graph Grammars / 12.3:
Typed Attributed Graph Transformation with Inheritance / 13:
Attributed Type Graphs with Inheritance / 13.1:
Attributed Clan Morphisms / 13.2:
Productions and Attributed Graph Transformation with Inheritance / 13.3:
Equivalence of Concepts with and without Inheritance / 13.4:
Case Study on Model Transformation, and Tool Support by AGG / Part IV:
Case Study on Model Transformation / 14:
Model Transformation by Typed Attributed Graph Transformation / 14.1:
Model Transformation from Statecharts to Petri Nets / 14.2:
Source Modeling Language: Simple Version of UML Statecharts / 14.2.1:
Target Modeling Language: Petri Nets / 14.2.2:
Model Transformation / 14.2.3:
Termination Analysis of the Model Transformation / 14.2.4:
Further Case Studies / 14.3:
From the General Resource Model to Petri Nets / 14.3.1:
From Process Interaction Diagrams to Timed Petri Nets / 14.3.2:
Conclusion / 14.4:
Implementation of Typed Attributed Graph Transformation by AGG / 15:
Language Concepts of AGG / 15.1:
Graphs / 15.1.1:
Typing Facilities / 15.1.2:
Node and Edge Attributes / 15.1.3:
Rules and Matches / 15.1.4:
Graph Transformations / 15.1.5:
Graph Grammars / 15.1.6:
Analysis Techniques Implemented in AGG / 15.2:
Graph Constraints / 15.2.1:
Critical Pair Analysis / 15.2.2:
Graph Parsing / 15.2.3:
Termination / 15.2.4:
Tool Environment of AGG / 15.3:
Visual Environment / 15.3.1:
Graph Transformation Engine / 15.3.2:
Tool Integration / 15.3.3:
A Short Introduction to Category Theory / 15.4:
Categories / A.1:
Construction of Categories, and Duality / A.2:
Monomorphisms, Epimorphisms, and Isomorphisms / A.3:
Pushouts and Pullbacks / A.4:
Binary Coproducts and Initial Objects / A.5:
Functors, Functor Categories, and Comma Categories / A.6:
Isomorphism and Equivalence of Categories / A.7:
A Short Introduction to Signatures and Algebras / B:
Algebraic Signatures / B.1:
Algebras / B.2:
Terms and Term Evaluation / B.3:
Detailed Proofs / C:
Completion of Proof of Fact 4.24 / C.1:
Proof of Lemma 6.25 / C.2:
Completion of Proof of Theorem 11.3 / C.3:
Well-Definedness / C.3.1:
Functors / C.3.2:
Isomorphism / C.3.3:
Proof of Lemma 11.17 / C.4:
Pushout Property / C.4.1:
Initial Pushout / C.4.3:
Proof of Theorem 13.12 / C.5:
Proof of Lemma 13.20 / C.6:
References
Index
Introduction to Graph Transformation Systems / Part I:
General Introduction / 1:
General Overview of Graph Grammars and Graph Transformation / 1.1:
5.

電子ブック

EB
Junghuei; Jonoska, Natasha; Rozenberg, Grzegorz Chen, Junghuei Chen, Natasha Jonoska, Nata??a Jonoska, Grzegorz Rozenberg
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2006
所蔵情報: loading…
目次情報: 続きを見る
DNA Nanotechnology - Algorithmic Self-assembly / Part I:
Scaffolded DNA Origami: from Generalized Multicrossovers to Polygonal Networks / Paul W.K. Rothemund
A Fresh Look at DNA Nanotechnology / Zhaoxiang Deng ; Yi Chen ; Ye Tian ; Chengde Mao
DNA Nanotechnology: an Evolving Field / Hao Yan ; Yan Liu
Self-healing Tile Sets / Erik Winfree
Compact Error-Resilient Computational DNA Tilings / John H. Reif ; Sudheer Sahu ; Peng Yin
Forbidding-Enforcing Conditions in DNA Self-assembly of Graphs / Giuditta Franco ; Natasa Jonoska
Codes for DNA Nanotechnology / Part II:
Finding MFE Structures Formed by Nucleic Acid Strands in a Combinatorial Set / Mirela Andronescu ; Anne Condon
Involution Solid Codes / Lila Kari ; Kalpana Mahalingam
Test Tube Selection of Large Independent Sets of DNA Oligonucleotides / Russell Deaton ; Junghuei Chen ; Jin-Woo Kim ; Max H. Garzon ; David H. Wood
DNA Nanodevices / Part III:
DNA-Based Motor Work at Bell Laboratories / Bernard Yurke
Electronics, Nanowire and DNA / Jong-Shik Shin ; Niles A. PiercePart IV:
A Supramolecular Approach to Metal Array Programming Using Artificial DNA / Mitsuhiko Shionoya
Multicomponent Assemblies Including Long DNA and Nanoparticles - An Answer for the Integration Problem? / Andreas Wolff ; Andrea Csaki ; Wolfgang Fritzsche
Molecular Electronics: from Physics to Computing / Yongqiang Xue ; Mark A. Ratner
Other Bio-molecules in Self-assembly / Part V:
Towards an Increase of the Hierarchy in the Construction of DNA-Based Nanostructures Through the Integration of Inorganic Materials / Bruno Samor`i ; Giampaolo Zuccheri ; Anita Scipioni ; Pasquale De Santis
Adding Functionality to DNA Arrays: the Development of Semisynthetic DNA-Protein Conjugates / Christof M. Niemeyer
Bacterial Surface Layer Proteins: a Simple but Versatile Biological Self-assembly System in Nature / Dietmar Pum ; Margit Sara ; Bernhard Schuster ; Uwe B. Sleytr
Biomolecular Computational Models / Part VI:
Computing with Hairpins and Secondary Structures of DNA / Masami Hagiya ; Satsuki Yaegashi ; Keiichiro Takahashi
Bottom-up Approach to Complex Molecular Behavior / Milan N. Stojanovic
Aqueous Computing: Writing on Molecules Dissolved in Water / Tom Head ; Susannah Gal
Computations Inspired by Cells / Part VII:
Turing Machines with Cells on the Tape / Francesco Bernardini ; Marian Gheorghe ; Natalio Krasnogor ; Gheorghe Paun
Insights into a Biological Computer: Detangling Scrambled Genes in Ciliates / Andre R.O. Cavalcanti ; Laura F. Landweber
Modelling Simple Operations for Gene Assembly / Tero Harju ; Ion Petre ; Grzegorz Rozenberg
Appendix / Part VIII:
Publications / Nadrian C. Seeman
DNA Nanotechnology - Algorithmic Self-assembly / Part I:
Scaffolded DNA Origami: from Generalized Multicrossovers to Polygonal Networks / Paul W.K. Rothemund
A Fresh Look at DNA Nanotechnology / Zhaoxiang Deng ; Yi Chen ; Ye Tian ; Chengde Mao
6.

電子ブック

EB
Jorg Flum, Martin Grohe, Grzegorz Rozenberg, European Association for Theoretical Computer Science.
出版情報: Springer eBooks Computer Science , Dordrecht : Springer Berlin Heidelberg, 2006
所蔵情報: loading…
7.

電子ブック

EB
Dines Bj?ner, Dines Bjorner, Grzegorz Rozenberg
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2006
所蔵情報: loading…
目次情報: 続きを見る
Preface
General
Brief Guide to Volume 3
Acknowledgements
Opening / Part I:
The Triptych Paradigm / 1:
Delineations of Software Engineering / 1.1:
The Triptych of Software Engineering / 1.2:
Phases, Stages and Steps of Development / 1.3:
The Triptych Process Model - A First View / 1.4:
Conclusion to Chapter 1 / 1.5:
Bibliographical Notes / 1.6:
Exercises / 1.7:
Documents / 2:
Documentation Is All! / 2.1:
Kinds of Document Parts / 2.2:
Deliverables / 2.3:
Informative Document Parts / 2.4:
Descriptive Document Parts / 2.5:
Analytic Document Parts / 2.6:
Discussion / 2.7:
Conceptual Framework / 2.8:
Methods and Methodology / 3:
Method / 3.1:
Methodology / 3.2:
Method Constituents / 3.3:
Development Principles, Techniques and Tools / 3.4:
Models and Modelling / 3.5:
Introductory, Context-Setting Remarks / 4.1:
Model Attributes / 4.2:
Roles of Models / 4.3:
The Modelling Principle / 4.4:
Descriptions: Theory and Practice / 4.5:
Phenomena and Concepts / 5:
Introduction / 5.1:
Entities / 5.2:
Functions / 5.4:
Events and Behaviours / 5.5:
Choice on Modelling Phenomena and Concepts / 5.6:
On Defining and on Definitions / 5.7:
A Pragmatics of Definitions / 6.1:
Varieties of Philosophy Definitions / 6.2:
Preliminary Discussion / 6.3:
A Syntax of Formal Definitions / 6.4:
A Semantics of Formal Definitions / 6.5:
Jackson's Description Principles / 6.6:
Phenomena, Facts and Individuals / 7.1:
Designations / 7.2:
Explicit Definitions / 7.3:
Refutable Assertions / 7.4:
Discussion: Description Principles / 7.5:
Domain Engineering / 7.6:
Overview of Domain Engineering / 8:
A Review of Why Domain Engineering? / 8.1:
Overview of Part and Chapter / 8.3:
Domain Stakeholders and Their Perspectives / 8.4:
Domain Acquisition and Validation / 8.5:
Domain Analysis and Concept Formation / 8.6:
Domain Facets / 8.7:
Auxiliary Stages of Domain Development / 8.8:
The Domain Model Document / 8.9:
Further Structure of This Part / 8.10:
Domain Stakeholders / 8.11:
Stakeholders / 9.1:
Stakeholder Perspectives / 9.3:
Discussion: Stakeholders and Their Perspectives / 9.4:
Domain Attributes / 9.5:
Continuity, Discreteness and Chaos / 10.1:
Statics and Dynamics / 10.3:
Tangibility and Intangibility / 10.4:
One, Two, ..., Dimensionality / 10.5:
Domain Facilitators: Business Processes / 10.6:
Domain Intrinsics / 11.3:
Domain Support Technologies / 11.4:
Domain Management and Organisation / 11.5:
Domain Rules and Regulations / 11.6:
Domain Scripts / 11.7:
Domain Human Behaviour / 11.8:
Other Domain Facets? / 11.9:
Composition of Domain Models / 11.10:
Domain Acquisition / 11.11:
The Acquisition Process / 12.1:
Concept Formation / 12.3:
Consistencies, Conflicts and Completeness / 13.3:
From Analysis to Synthesis / 13.4:
Domain Verification and Validation / 13.5:
Domain Verification / 14.1:
Domain Validation / 14.3:
Towards Domain Theories / 14.4:
What Is a Domain Theory? / 15.1:
Example Statements of Domain Theories / 15.3:
Possible Domain Theories / 15.4:
How Do We Establish a Theory? / 15.5:
Purpose of a Domain Theory / 15.6:
Summary Principles, Techniques and Tools / 15.7:
The Domain Engineering Process Model / 15.8:
Review of Domain Development / 16.1:
Review of Domain Documents / 16.3:
Requirements Engineering / 16.4:
Overview of Requirements Engineering / 17:
Why Requirements, and for What? / 17.1:
Getting Started on Requirements Development / 17.3:
On Domains, Requirements and the Machine / 17.4:
Overview: Requirements Engineering Stages / 17.5:
The Requirements Document / 17.6:
The Structure of the Rest of the Part / 17.7:
Requirements Stakeholders / 17.8:
General Application Stakeholders / 18.1:
COTS Software House Stakeholders / 18.3:
Requirements Facets / 18.4:
Rough Sketching and Terminology / 19.1:
Business Process Reengineering Requirements / 19.3:
Domain Requirements / 19.4:
Interface Requirements / 19.5:
Machine Requirements / 19.6:
Composition of Requirements Models / 19.7:
Discussion: Requirements Facets / 19.8:
Requirements Acquisition / 19.9:
Requirements Acquisition Versus Domain Models / 20.1:
Domain Model-Based Requirements Acquisition / 20.2:
Overview of Concepts / 20.3:
Requirements Analysis and Concept Formation / 20.4:
Consistencies, Conflicts, and Completeness / 21.1:
Requirements Verification and Validation / 21.4:
Requirements Verification / 22.1:
Requirements Validation / 22.3:
Requirements Satisfiability and Feasibility / 22.4:
Satisfaction Study / 23.1:
Technical Feasibility Study / 23.3:
Economic Feasibility Study / 23.4:
Compliance with Implicit/Derivative Goals / 23.5:
The Requirements Engineering Process Model / 23.6:
Review of Requirements Development / 24.1:
Review of Requirements Documents / 24.3:
The Repeat Table of Contents Listing / 24.4:
Computing Systems Design / 24.5:
Hardware/Software Codesign / 25:
Introduction - On Architecture / 25.1:
Hardware Components and Modules / 25.2:
Software Components and Modules / 25.3:
Stepwise Refinement of Architectures / 25.4:
Principles, Techniques and Tools / 25.6:
Software Architecture Design / 26:
Initial Domain Requirements Architecture / 26.1:
Initial Machine Requirements Architecture / 26.3:
Analysis of Some Machine Requirements / 26.4:
Prioritisation of Design Decisions / 26.5:
Corresponding Designs / 26.6:
A Case Study in Component Design / 26.7:
Overview Introduction / 27.1:
Overview of Example / 27.2:
Methodology Overview / 27.3:
Step 0: Files and Pages / 27.4:
Step 1: Catalogue, Disk and Storage / 27.5:
Step 2: Disks / 27.6:
Step 3: Caches / 27.7:
Step 4: Storage Crashes / 27.8:
Step 5: Flattening Storage and Disks / 27.9:
Step 6: Disk Space Management / 27.10:
Domain-Specific Architectures / 27.11:
Translator Architectures / 28.1:
Information Repository Architectures / 28.3:
Client/Server Architectures / 28.4:
Workpiece Architectures / 28.5:
Reactive System Architectures / 28.6:
Connection Frame / 28.7:
Etcetera: Coding and All That! / 28.8:
From Formal Specification to Programming / 29.1:
The Beauty of Programming / 29.2:
Programming Practices / 29.3:
Confidence-Building Software Development / 29.4:
Verification, Model Checking and Testing / 29.5:
The Computing Systems Design Process Model / 29.6:
Review of Software Design / 30.1:
Review of Software Design Documents / 30.3:
Closing / 30.4:
The Triptych Development Process Model / 31:
Phase Process Models / 31.1:
Phase Documentation Table of Contents / 31.2:
Conclusion / 31.3:
Finale / 32:
Informal and Formal Software Engineering / 32.1:
Myths and Commandments of Formal Methods / 32.2:
FAQs: Frequently Asked Questions / 32.3:
Research and Tool Development / 32.4:
Application Areas / 32.5:
Closing Remarks / 32.6:
Appendixes / Part VIII:
An RSL Primer / A:
Types / A.1:
The RSL Predicate Calculus / A.2:
Concrete RSL Types / A.3:
[lambda]-Calculus and Functions / A.4:
Further Applicative Expressions / A.5:
Imperative Constructs / A.6:
Process Constructs / A.7:
Simple RSL Specifications / A.8:
Glossary / B:
Indexes / C:
Concepts Index / C.1:
Characterisations and Definitions Index / C.2:
Authors Index / C.3:
References
Preface
General
Brief Guide to Volume 3
8.

電子ブック

EB
Wilfried Brauer, Hartmut Ehrig, Grzegorz Rozenberg, Karsten Ehrig, Ulrike Prange, Gabriele Taentzer
出版情報: SpringerLink Books - AutoHoldings , Springer Berlin Heidelberg, 2006
所蔵情報: loading…
目次情報: 続きを見る
Introduction to Graph Transformation Systems / Part I:
General Introduction / 1:
General Overview of Graph Grammars and Graph Transformation / 1.1:
What Is Graph Transformation? / 1.1.1:
Aims and Paradigms of Graph Transformation / 1.1.2:
Overview of Various Approaches / 1.1.3:
The Main Ideas of the Algebraic Graph Transformation Approach / 1.2:
The DPO Approach / 1.2.1:
The Algebraic Roots / 1.2.2:
From the DPO to the SPO Approach / 1.2.3:
From Graphs to High-Level Structures / 1.2.4:
The Chapters of This Book and the Main Results / 1.3:
Part I: Introduction to Graph Transformation Systems / 1.3.1:
Part II: Adhesive HLR Categories and Systems / 1.3.2:
Part III: Typed Attributed Graph Transformation Systems / 1.3.3:
Part IV: Case Study and Tool Support / 1.3.4:
Appendices / 1.3.5:
Hints for Reading This Book / 1.3.6:
Bibliographic Notes and Further Topics / 1.4:
Concepts of Graph Grammars and Graph Transformation Systems / 1.4.1:
Application Areas of Graph Transformation Systems / 1.4.2:
Languages and Tools for Graph Transformation Systems / 1.4.3:
Future Work / 1.4.4:
Graphs, Typed Graphs, and the Gluing Construction / 2:
Graphs and Typed Graphs / 2.1:
Introduction to Categories / 2.2:
Pushouts as a Gluing Construction / 2.3:
Pullbacks as the Dual Construction of Pushouts / 2.4:
Graph Transformation Systems / 3:
Basic Definitions for GT Systems / 3.1:
Construction of Graph Transformations / 3.2:
Local Church-Rosser and Parallelism Theorems for GT Systems / 3.3:
Overview of Some Other Main Results for GT Systems / 3.4:
Concurrency Theorem / 3.4.1:
Embedding and Extension Theorems / 3.4.2:
Confluence, Local Confluence, Termination, and Critical Pairs / 3.4.3:
Functional Behavior of GT Systems and Termination Analysis / 3.4.4:
Graph Constraints and Application Conditions / 3.5:
Adhesive High-Level Replacement Categories and Systems / Part II:
Adhesive High-Level Replacement Categories / 4:
Van Kampen Squares and Adhesive Categories / 4.1:
Adhesive HLR Categories / 4.2:
HLR Properties of Adhesive HLR Categories / 4.3:
Adhesive High-Level Replacement Systems / 5:
Basic Concepts of Adhesive HLR Systems / 5.1:
Instantiation of Adhesive HLR Systems / 5.2:
Graph and Typed Graph Transformation Systems / 5.2.1:
Hypergraph Transformation Systems / 5.2.2:
Petri Net Transformation Systems / 5.2.3:
Algebraic Specification Transformation Systems / 5.2.4:
Typed Attributed Graph Transformation Systems / 5.2.5:
The Local Church-Rosser and Parallelism Theorems / 5.3:
Concurrency Theorem and Pair Factorization / 5.4:
Embedding and Local Confluence / 6:
Initial Pushouts and the Gluing Condition / 6.1:
Critical Pairs / 6.2:
Local Confluence Theorem / 6.4:
Constraints and Application Conditions / 7:
Definition of Constraints and Application Conditions / 7.1:
Construction of Application Conditions from Constraints / 7.2:
Construction of Left from Right Application Conditions / 7.3:
Guaranteeing and Preservation of Constraints / 7.4:
Typed Attributed Graphs / Part III:
Attributed Graphs and Typing / 8.1:
Pushouts as a Gluing Construction of Attributed Graphs / 8.2:
Pullbacks of Attributed Graphs / 8.3:
Basic Concepts for Typed AGT Systems / 9:
Construction of Typed Attributed Graph Transformations / 9.2:
Local Church-Rosser and Parallelism Theorem for Typed AGT Systems / 9.3:
Concurrency Theorem and Pair Factorization for Typed AGT Systems / 9.4:
Pair Factorizations / 9.4.1:
Embedding and Local Confluence for Typed AGT Systems / 9.4.2:
Embedding and Extension Theorems for Typed AGT Systems / 10.1:
Critical Pairs for Typed AGT Systems / 10.2:
Local Confluence Theorem for Typed AGT Systems / 10.3:
Adhesive HLR Categories for Typed Attributed Graphs / 11:
Attributed Graph Structure Signatures and Typed Attributed Graphs / 11.1:
Definition of Concrete Adhesive HLR Categories / 11.2:
Verification of the Main Results for Typed AGT Systems / 11.3:
Constraints, Application Conditions and Termination for TAGT Systems / 12:
Constraints and Application Conditions for Typed AGT Systems / 12.1:
Equivalence of Constraints and Application Conditions / 12.2:
Termination Criteria for Layered Typed Attributed Graph Grammars / 12.3:
Typed Attributed Graph Transformation with Inheritance / 13:
Attributed Type Graphs with Inheritance / 13.1:
Attributed Clan Morphisms / 13.2:
Productions and Attributed Graph Transformation with Inheritance / 13.3:
Equivalence of Concepts with and without Inheritance / 13.4:
Case Study on Model Transformation, and Tool Support by AGG / Part IV:
Case Study on Model Transformation / 14:
Model Transformation by Typed Attributed Graph Transformation / 14.1:
Model Transformation from Statecharts to Petri Nets / 14.2:
Source Modeling Language: Simple Version of UML Statecharts / 14.2.1:
Target Modeling Language: Petri Nets / 14.2.2:
Model Transformation / 14.2.3:
Termination Analysis of the Model Transformation / 14.2.4:
Further Case Studies / 14.3:
From the General Resource Model to Petri Nets / 14.3.1:
From Process Interaction Diagrams to Timed Petri Nets / 14.3.2:
Conclusion / 14.4:
Implementation of Typed Attributed Graph Transformation by AGG / 15:
Language Concepts of AGG / 15.1:
Graphs / 15.1.1:
Typing Facilities / 15.1.2:
Node and Edge Attributes / 15.1.3:
Rules and Matches / 15.1.4:
Graph Transformations / 15.1.5:
Graph Grammars / 15.1.6:
Analysis Techniques Implemented in AGG / 15.2:
Graph Constraints / 15.2.1:
Critical Pair Analysis / 15.2.2:
Graph Parsing / 15.2.3:
Termination / 15.2.4:
Tool Environment of AGG / 15.3:
Visual Environment / 15.3.1:
Graph Transformation Engine / 15.3.2:
Tool Integration / 15.3.3:
A Short Introduction to Category Theory / 15.4:
Categories / A.1:
Construction of Categories, and Duality / A.2:
Monomorphisms, Epimorphisms, and Isomorphisms / A.3:
Pushouts and Pullbacks / A.4:
Binary Coproducts and Initial Objects / A.5:
Functors, Functor Categories, and Comma Categories / A.6:
Isomorphism and Equivalence of Categories / A.7:
A Short Introduction to Signatures and Algebras / B:
Algebraic Signatures / B.1:
Algebras / B.2:
Terms and Term Evaluation / B.3:
Detailed Proofs / C:
Completion of Proof of Fact 4.24 / C.1:
Proof of Lemma 6.25 / C.2:
Completion of Proof of Theorem 11.3 / C.3:
Well-Definedness / C.3.1:
Functors / C.3.2:
Isomorphism / C.3.3:
Proof of Lemma 11.17 / C.4:
Pushout Property / C.4.1:
Initial Pushout / C.4.3:
Proof of Theorem 13.12 / C.5:
Proof of Lemma 13.20 / C.6:
References
Index
Introduction to Graph Transformation Systems / Part I:
General Introduction / 1:
General Overview of Graph Grammars and Graph Transformation / 1.1:
9.

電子ブック

EB
Drewes, Grzegorz Rozenberg, Arto Salomaa
出版情報: SpringerLink Books - AutoHoldings , Springer Berlin Heidelberg, 2006
所蔵情報: loading…
目次情報: 続きを見る
Introduction / 1:
The Tree-Based Approach / 1.1:
From Strings to Trees / 1.2:
Picture Algebras / 1.3:
Organization and Content of the Chapters / 1.4:
Other Formalisms for Picture Generation / 1.5:
Line-Drawing Languages / 2:
Four Lines and a Concatenation Operation / 2.1:
Context-Free Chain-Code Picture Languages / 2.2:
Classes of Chain-Code Picture Languages / 2.3:
Analysing Chain-Code Picture Languages / 2.4:
ET0L Chain-Code Picture Languages / 2.5:
The Turtle Operations / 2.6:
Extensions / 2.7:
Bibliographic Remarks / 2.8:
Collage Languages / 3:
Basic Definitions and Examples / 3.1:
Properties of Context-Free Collage Languages / 3.2:
Parallel Replacement / 3.3:
Tilings / 3.4:
A Case Study: Generating Celtic Knotwork / 3.5:
Iterated Function Systems / 3.6:
Compact Subsets of Complete Metric Spaces / 4.1:
Fractal Curves / 4.2:
Networked Iterated Function Systems / 4.4:
Grid Picture Languages / 4.5:
Context-Free and ET0L Grid Picture Languages / 5.1:
Raster Images of Grid Pictures / 5.2:
Beyond ET0L / 5.3:
Grid NIFss / 5.4:
More General Grids / 5.5:
Languages of Fractals / 5.6:
Infinite Trees and Their Value / 6.1:
T0L Function Systems / 6.2:
Branching-Synchronization Function Systems / 6.3:
Languages of Coloured Collages / 6.4:
Collage Grammars with Colour Attributes / 7.1:
Continuous Colourings / 7.2:
Parametrized Colour Operations / 7.3:
Treebag / 7.4:
A Bird's-Eye View of Treebag / 8.1:
Selected Examples / 8.2:
A Worm's-Eye View of Treebag / 8.3:
Introduction to Tree Languages / A:
Trees / A.1:
Regular Tree Languages / A.2:
ET0L Tree Languages / A.3:
Branching Tree Languages / A.4:
Top-Down and Bottom-Up Tree Transformations / A.5:
Tree Transducers Defining Tree Languages / A.6:
Constructing Trees by Substitution / A.7:
Notation / B:
Basic Mathematical Notation / B.1:
Strings, Trees, and Pictures / B.2:
References
Index
Introduction / 1:
The Tree-Based Approach / 1.1:
From Strings to Trees / 1.2:
10.

電子ブック

EB
Andrea Corradini, Hartmut Ehrig, Takeo Kanade, Ugo Montanari, Leila Ribeiro, Grzegorz Rozenberg
出版情報: SpringerLink Books - AutoHoldings , Springer Berlin Heidelberg, 2006
所蔵情報: loading…
文献の複写および貸借の依頼を行う
 文献複写・貸借依頼