Table of Contents

2.1. Overview

2.2. System

2.3. Identifiers

2.4. Types

2.4.1. Primitive Types

2.4.2. Non-Primitive Types

2.4.3. Alias Type

2.4.4. Generic Type

2.4.5. Fun Type

2.5. Literals

2.6. Constant Declaration

2.7. Enumeration Declaration

2.8. Record Declaration

2.9. Extension Declaration

2.9.1. Type Extension Declaration

2.9.2. Expression Extension Declaration

2.9.3. Action Extension Declaration

2.10. Type-alias Declaration

2.11. Global Variable Declaration

2.12. Thread and Function Declarations

2.12.1. Parameters and Local Variables

2.13. Low-level Thread or Function Body

2.13.1. Location

2.13.2. Transformation

2.13.3. Jump

2.13.4. Catch

2.14. High-level Thread or Function Body

2.14.1. Statement

2.15. Virtual Table Declaration

2.15.1. Record-based

2.15.2. Enumeration-based

2.16. Functional Expression Declaration

2.17. Expressions

2.17.1. Literal Expressions

2.17.2. Variable Expression

2.17.3. Unary Expression

2.17.4. Binary Expression

2.17.5. Conditional Expression

2.17.6. Parenthesis Expression

2.17.7. Atomic Expression

2.17.8. Record, Array, and Lock Creation Expressions

2.17.9. Field Access Expression

2.17.10. Array Access Expression

2.17.11. Cast Expression

2.17.12. Kind-of Expression

2.17.13. Instance-of Expression

2.17.14. Lock Test Expressions

2.17.15. Thread Test Expression

2.17.16. Let Binding Expression

2.17.17. Application Expression

2.17.18. Extension Call Expression

2.18. Actions

2.18.1. Assign Action

2.18.2. Assert Action

2.18.3. Assume Action

2.18.4. Lock Operation Action

2.18.5. Throw Exception Action

2.18.6. Start Thread Action

2.18.7. Exit Thread Action

2.18.8. Extension Call Action