otherwise
guard more than onceotherwise
guard with non-guard statementsillegal
with imperative statementsillegal
in if
-statementillegal
in functionport
not boundport
not bound – of instance
port
is bound more than onceinstance
in in a cyclic bindingrequires
portexternal
port to non-external
portNext: Introduction [Contents][Index]
This document describes Dezyne version 2.17.2.
• Introduction | What is Dezyne about? | |
• Ideas and Concepts | Explaining the underlying thinking. | |
• Installation | Installing Dezyne. | |
• Getting Started | Writing a program in Dezyne. | |
• Execution Semantics | How do they do it? | |
• Formal Verification | A guide to verification errors. | |
• Defensive Design | A protective armor. | |
• Code Integration | Creating an executable. | |
• The Dezyne command-line tools | Running the tools. | |
• Dezyne Language Reference | All the language details. | |
• Well-formedness | Interpreting parse errors. | |
• Contributing | Your help needed! | |
• Concept Index | Concepts. | |
• GNU Free Documentation License | The license of this manual. | |
— The Detailed Node Listing — Introduction | ||
---|---|---|
• Purpose | Why are we creating Dezyne? | |
• Conditions for Using Dezyne | There are (almost) no limits to using Dezyne. | |
Ideas and Concepts | ||
• Concurrency | A message passing programming model. | |
• Component Based | Recursive decompositioning. | |
• Model Based | Modeling the real world. | |
• Design by Contract | Contracts for message interaction. | |
• Managing Complexity | Abstraction and encapsulation. | |
Installation | ||
• Requirements | Software needed to build and run Dezyne. | |
Getting Started | ||
• Hello World! | First contact with Dezyne. | |
• A Simple State Machine | Stateful behavior and protocol. | |
• A Camera Example | A System of Components and Systems. | |
• The Lego Ball Sorter | A Machine Operating System. | |
Execution Semantics | ||
• Direct in event | A provides trigger forwarded | |
• Direct out event | A requires trigger forwarded. | |
• Direct multiple out events | Multiple requires triggers forwarded. | |
• Indirect in event | A requires trigger => requires action. | |
• Indirect out event | A provides trigger => provides trigger via requires action. | |
• Indirect multiple out events | Provides trigger => provides trigger via requires actions and triggers. | |
• Indirect blocking out event | Synchronize two triggers via block and release. | |
• External multiple out events | Delay caused by parallelism | |
• Indirect blocking multiple external out events | Block, delay, release. | |
• Multiple provides | Multiple provides ports | |
• Blocking multiple provides | Blocking and multiple provides ports | |
• Blocking in system context | Blocking by one level of indirection: collateral blocking | |
Formal Verification | ||
• Verification Checks and Errors | Which properties are verified? | |
• Verification Counter Examples | What if verification fails? | |
• Interpreting Verification Errors | How to fix verification errors. | |
Defensive Design | ||
• Interface Contracts | Consequences of a breach of contract. | |
• Error Handling and Recovery | Specifying Exceptional behavior. | |
• Armoring | Making a program robust. | |
Code Integration | ||
• Integrating C++ Code | ||
• Foreign Component | ||
• Thread-safe Shell | ||
• Integrating Scheme Code | ||
Integrating Scheme Code | ||
• Namespace to Module | ||
The Dezyne command-line tools | ||
• Invoking dzn | Running Dezyne commands. | |
• Invoking dzn code | Generating code from a Dezyne file. | |
• Invoking dzn graph | Generating graphs of Dezyne models. | |
• Invoking dzn hello | A simple sanity check. | |
• Invoking dzn language | Lookup and completion. | |
• Invoking dzn lts | Manipulate and query an LTS. | |
• Invoking dzn parse | Checking the syntax of Dezyne file. | |
• Invoking dzn simulate | Simulating Dezyne models. | |
• Invoking dzn trace | Transform verify, code, and simulate traces. | |
• Invoking dzn traces | Generate a set of traces. | |
• Invoking dzn verify | Verifying Dezyne models. | |
Dezyne Language Reference | ||
• Lexical Analysis | Tokens, separators and whitespace. | |
• Dezyne Files | What goes into a Dezyne file? | |
• Types and Expressions | Manipulating data in Dezyne. | |
• Interfaces | Defining contracts for components and systems. | |
• Components | Defining a program’s behavior in Dezyne. | |
• Systems | Decomposing a system. | |
• Namespaces | Avoiding name collision. | |
Lexical Analysis | ||
• Identifiers | Choosing names. | |
• Keywords | Restricted words. | |
• Operators | Building blocks for expressions. | |
• Delimiters | Constructing lists. | |
• Lexical Scoping | Locality of names. | |
• Comments | Explanations for human readers. | |
Types and Expressions | ||
• Void | Definitions without type. | |
• Bool | Builtin boolean type. | |
• Enum | Enumerated user types. | |
• Subint | Integer user types. | |
• Extern Data Type | Foreign data user types. | |
• Expressions | Constants and data. | |
Interfaces | ||
• Events | Event or message definitions. | |
• Behavior | Specifying an interface protocol. | |
• Declarative Statements | Define when to run which trigger. | |
• Imperative Statements | The code that runs upon a trigger. | |
• Functions | Avoiding code duplication. | |
Behavior | ||
• Behavior Variable | The detailed state of the behavior. | |
Declarative Statements | ||
• On | Defining what happens upon a trigger. | |
• Guard | Declarative trigger condition. | |
• Using inevitable and optional | Nitty gritty details on using modeling events. | |
Imperative Statements | ||
• Action | Emitting events. | |
• Assign | Updating state. | |
• Function Call | A named collection of imperative statements. | |
• Empty Statement | When a trigger has no effect, or there is nothing to do. | |
• If | Imperative decisions. | |
• Illegal | Specifying what is not allowed. | |
• Reply | Determining the reply for a valued trigger. | |
• Return | Returning from a function. | |
• Variable | Defining a local variable. | |
Components | ||
• Ports | Defining a component’s communication channels. | |
• Component Behavior | Defining a component’s behavior. | |
• Component Types | Three types of components. | |
• Component Declarative Statements | Component-specific declarative statements. | |
• Component Imperative Statements | Component-specific imperative statements. | |
• Multiple Provides Ports | Providing more than one interface. | |
Ports | ||
• Injection | Ports sharing a resource. | |
• External | Ports with external delay. | |
Component Declarative Statements | ||
• Component On | Defining what happens on a trigger. | |
• Blocking | Implementing a synchronous call on decoupled events. | |
• Formal Binding | Parameter assignment in blocking or synchronous out context. | |
• Joining Activities | A full blocking example. | |
Component Imperative Statements | ||
• Component Action | Sending messages over ports. | |
• Component If | Imperative decisions in a component. | |
• Component Illegal | Using illegal in a component. | |
• Component Reply | Using reply in a component. | |
• Component Defer | Decoupling execution from the client. | |
Systems | ||
• Component Instances | The components of a system. | |
• Binding | The plumbing of a system. | |
Binding | ||
• Using Injection | Binding injected ports. | |
Well-formedness | ||
• Well-formedness Checks Categories | Types of checks. | |
• List of Well-formedness Checks | An alphabetical lookup list. | |
• Well-formedness -- Top level | Interfaces, events and components. | |
• Well-formedness -- Directional | Direction of trigger and action. | |
• Well-formedness -- Nesting | The right place for declarative and imperative. | |
• Well-formedness -- Mixing | Mixing of declarative and imperative. | |
• Well-formedness -- Reply | Reply and ports. | |
• Well-formedness -- Valued Actions and Calls | Careful use of values. | |
• Well-formedness -- Injection | Restrictions on injection. | |
• Well-formedness -- Functions | Returning and recursing. | |
• Well-formedness -- Data Parameters | Data type errors. | |
• Well-formedness -- System | Correctly binding all ports. | |
Well-formedness – Top level | ||
• Interface must define an event | ||
• Interface must define a behavior | ||
• Out-event must be void | ||
• Component with behavior must have a trigger | ||
• Component with behavior must define a provides port | ||
Well-formedness – Directional | ||
• Cannot use event as action | ||
• Cannot use event as trigger | ||
Well-formedness – Nesting | ||
• Assign outside on | ||
• Action outside on | ||
• Nested on used | ||
• Nested blocking used | ||
• Cannot use blocking in an interface | ||
Well-formedness – Mixing | ||
• Declarative statement expected | ||
• Imperative statement expected | ||
• Cannot use otherwise guard more than once | ||
• Cannot use otherwise guard with non-guard statements | ||
• Cannot use illegal with imperative statements | ||
• Cannot use illegal in if-statement | ||
• Cannot use illegal in function | ||
Well-formedness – Reply | ||
• Must specify provides-port with reply on out-trigger | ||
• Must specify provides-port with reply | ||
Well-formedness – Valued Actions and Calls | ||
• Action in member variable initializer | ||
• Call in member variable initializer | ||
• Action value discarded | ||
• Call value discarded | ||
Well-formedness – Injection | ||
• Injected port has out-events | ||
Well-formedness – Functions | ||
• Missing return | ||
• Cannot use return outside of function | ||
• Cannot use statement after recursive call | ||
Well-formedness – Data Parameters | ||
• Type mismatch -- parameter expected extern | ||
• Cannot use out-parameter on out-event | ||
• Cannot use inout-parameter on out-event | ||
• Formal binding is not a data member variable | ||
Well-formedness – System | ||
• Port not bound | ||
• Port not bound -- of instance | ||
• Port is bound more than once | ||
• Cannot bind port to port | ||
• Cannot bind two wildcards | ||
• Instance is in a cyclic binding | ||
• Cannot bind wildcard to requires port | ||
• System composition is recursive | ||
• Cannot bind external port to non-external port | ||
Contributing | ||
• Building from Git | The latest and greatest. | |
• Running Dezyne Before It Is Installed | Hacker tricks. | |
• The Perfect Setup | The right tools. | |
• Coding Style | Hygiene of the contributor. | |
• Submitting Patches | Share your work. | |
Coding Style | ||
• Programming Paradigm | How to compose your elements. | |
• Data Types and Pattern Matching | Implementing data structures. | |
• Formatting Code | Writing conventions. | |
Next: Introduction [Contents][Index]