Dezyne 参考手册

下一篇: 导论 [目录][索引]

Dezyne

本文档描述的是 Dezyne 2.18.3 版本。

目录

• 1 导论
  • 1.1 目的
  • 1.2 使用 Dezyne 的条件
• 2 思想和概念
  • 2.1 并发性
  • 2.2 基于组件
  • 2.3 基于模型
  • 2.4 契约式设计
  • 2.5 管理复杂性
• 3 安装
  • 3.1 要求
• 4 快速入门
  • 4.1 Hello World!
  • 4.2 简单状态机
  • 4.3 相机示例
  • 4.4 Lego 球分类器
• 5 执行语义
  • 5.1 直接 in event
  • 5.2 直接 out event
  • 5.3 直接 multiple out events
  • 5.4 间接 in event
  • 5.5 间接 out event
  • 5.6 间接 multiple out events
  • 5.7 间接 blocking out event
  • 5.8 外部 multiple out events
  • 5.9 间接 blocking multiple external out events
  • 5.10 Multiple provides
  • 5.11 Blocking multiple provides
  • 5.12 在系统上下文中 Blocking
    • 5.12.1 Collateral blocking 和 multiple provides.
• 6 形式化验证
  • 6.1 验证检查和错误
  • 6.2 验证反例
  • 6.3 解释验证错误
• 7 防御性设计
  • 7.1 接口契约
    • 7.1.1 隐式接口约束
    • 7.1.2 共享接口变量
  • 7.2 错误处理和恢复
  • 7.3 Armoring
• 8 代码集成
  • 8.1 集成 C++ 代码
    • 8.1.1 导论
    • 8.1.2 接口
    • 8.1.3 组件
    • 8.1.4 系统
    • 8.1.5 集成
  • 8.2 外部组件
  • 8.3 线程安全 Shell
    • 8.3.1 Shell 语法
    • 8.3.2 语义
    • 8.3.3 Shell 示例
    • 另请参阅：
  • 8.4 集成 Scheme 代码
    • 8.4.1 Namespace to Module
• 9 Dezyne 命令行工具
  • 9.1 调用 dzn
  • 9.2 调用 dzn code
  • 9.3 调用 dzn graph
  • 9.4 调用 dzn hello
  • 9.5 调用 dzn language
  • 9.6 调用 dzn lts
  • 9.7 调用 dzn parse
  • 9.8 调用 dzn simulate
  • 9.9 调用 dzn trace
  • 9.10 调用 dzn traces
  • 9.11 调用 dzn verify
• 10 Dezyne 语言参考
  • 10.1 词法分析
    • 10.1.1 标识符
    • 10.1.2 关键字
    • 10.1.3 运算符
    • 10.1.4 分隔符
    • 10.1.5 词法作用域
    • 10.1.6 注释
  • 10.2 Dezyne 文件
    • 10.2.1 Import
  • 10.3 类型和表达式
    • 10.3.1 void
    • 10.3.2 bool
    • 10.3.3 enum
    • 10.3.4 subint
    • 10.3.5 extern data
    • 10.3.6 表达式
  • 10.4 接口
    • 10.4.1 Events
      • 10.4.1.1 Modeling Events
    • 10.4.2 Behavior
      • 10.4.2.1 Behavior variable
    • 10.4.3 Declarative Statements
      • 10.4.3.1 on
      • 10.4.3.2 guard
      • 10.4.3.3 Using inevitable and optional
    • 10.4.4 Imperative Statements
      • 10.4.4.1 action
      • 10.4.4.2 assign
      • 10.4.4.3 call
      • 10.4.4.4 Empty Statement
      • 10.4.4.5 if
      • 10.4.4.6 illegal
      • 10.4.4.7 reply
      • 10.4.4.8 return
      • 10.4.4.9 variable
    • 10.4.5 Functions
  • 10.5 组件
    • 10.5.1 Ports
      • 10.5.1.1 Injection
      • 10.5.1.2 external
      • 10.5.1.3 Race condition due to external delay
    • 10.5.2 Component Behavior
    • 10.5.3 Component Types
      • 10.5.3.1 A Leaf Component
      • 10.5.3.2 A Foreign Component
      • 10.5.3.3 A System Component
    • 10.5.4 Component Declarative Statements
      • 10.5.4.1 Component on
      • 10.5.4.2 blocking
      • 10.5.4.3 Formal Binding
      • 10.5.4.4 Joining Activities
    • 10.5.5 Component Imperative Statements
      • 10.5.5.1 Component action
      • 10.5.5.2 Component if
      • 10.5.5.3 Component illegal
      • 10.5.5.4 Component reply
      • 10.5.5.5 Component defer
    • 10.5.6 Multiple Provides Ports
  • 10.6 系统
    • 10.6.1 Component Instances
    • 10.6.2 Binding
      • 10.6.2.1 Using Injection
  • 10.7 Namespaces
    • 10.7.1 Namespace Extension
    • 10.7.2 Referencing
• 11 良好形式
  • 11.1 Well-formedness Checks Categories
  • 11.2 List of Well-formedness Checks
  • 11.3 Well-formedness – Top level
    • 11.3.1 Interface must define an event
    • 11.3.2 Interface must define a behavior
    • 11.3.3 out-event must be void
    • 11.3.4 Component with behavior must have a trigger
    • 11.3.5 Component with behavior must define a provides port
  • 11.4 Well-formedness – Directional
    • 11.4.1 Cannot use event as action
    • 11.4.2 Cannot use event as trigger
  • 11.5 Well-formedness – Nesting
    • 11.5.1 assign outside on
    • 11.5.2 action outside on
    • 11.5.3 Nested on used
    • 11.5.4 Nested blocking used
    • 11.5.5 Cannot use blocking in an interface
  • 11.6 Well-formedness – Mixing
    • 11.6.1 Declarative statement expected
    • 11.6.2 Imperative statement expected
    • 11.6.3 Cannot use otherwise guard more than once
    • 11.6.4 Cannot use otherwise guard with non-guard statements
    • 11.6.5 Cannot use illegal with imperative statements
    • 11.6.6 Cannot use illegal in if-statement
    • 11.6.7 Cannot use illegal in function
  • 11.7 Well-formedness – Reply
    • 11.7.1 Must specify provides-port with reply on out-trigger
    • 11.7.2 Must specify provides-port with reply
  • 11.8 Well-formedness – Valued Actions and Calls
    • 11.8.1 action in member variable initializer
    • 11.8.2 call in member variable initializer
    • 11.8.3 action value discarded
    • 11.8.4 call value discarded
  • 11.9 Well-formedness – Injection
    • 11.9.1 injected port has out-events
  • 11.10 Well-formedness – Functions
    • 11.10.1 Missing return
    • 11.10.2 Cannot use return outside of function
    • 11.10.3 Cannot use statement after recursive call
  • 11.11 Well-formedness – Data Parameters
    • 11.11.1 Type mismatch: parameter expected extern
    • 11.11.2 Cannot use out-parameter on out-event
    • 11.11.3 Cannot use inout-parameter on out-event
    • 11.11.4 Formal binding is not a data member variable
  • 11.12 Well-formedness – System
    • 11.12.1 port not bound
    • 11.12.2 port not bound – of instance
    • 11.12.3 port is bound more than once
    • 11.12.4 Cannot bind port to port
    • 11.12.5 Cannot bind two wildcards
    • 11.12.6 instance in in a cyclic binding
    • 11.12.7 Cannot bind wildcard to requires port
    • 11.12.8 System composition is recursive
    • 11.12.9 Cannot bind external port to non-external port
• 12 贡献
  • 12.1 从 Git 构建
  • 12.2 在安装之前运行 Dezyne
  • 12.3 完美设置
  • 12.4 编码风格
    • 12.4.1 编程范例
    • 12.4.2 数据类型和模式匹配
    • 12.4.3 格式化代码