Contents

• Introduction
  • Toolchain Flow
  • Bundles
  • Binding and Naming
  • DoP and Checking Granularity
  • Re-Hydration
  
  
• Ontology
  • Glossary
  
  
• Pushlogic Constants
  • Atomic Constant Values.
  • Event Constants
  • Pushlogic Types
    • Lock Type
    • Fuse Type
    • Boolean Type
  
  
• Pushlogic Object Level (VM Execution)
  • Code Reflection Schema
  • Virtual Machine
  • Pushlogic Expressions
  • Fields and their Declaration.
  • Level and Event Expressions
    • Syntax-directed guide to level and event expressions
    • Assertions on Level and Event Expressions
  • Executable Rules
    • Nominal Meaning of a Rule
    • Event and Level Constraints
    • Unilateral Reset to Safe Value
    • Pushbacks: Simple and Complex Undo
    • Complex Undo
  • Inter-Bundle Communication
  • Standing Constraints
  • Temporal Logic Assertions
  
  
• Pushlogic Source Language
  • Concrete syntax tree
  • Abstract syntax tree
  • Program File
  • Bundle Declaration
  • Constant Values
  • Identifiers
  • Field Declarations
    • Sort Statement
    • Namespace Binding
  • Pragmas
  • Operators
    • Function Call
  • Pushlogic Statements
    • Emit Statement (SOAP and GENA too)
    • Pebble Statement
    • Input and Output Statements
    • Assignment Statement
    • Sequential composition
    • With Statement
    • If/Then/Else Statement
    • Switch/Case/Default Statement
    • Stategraph Statement
    • Disable Statement
    • While/For/Break/Continue Statements
    • Procedure Call Statement
    • Return Statement
    • Wait Statement
    • Lock Statement
    • Fuse Statement
  • Pushlogic RPC
    • Foreign RPC (SOAP and GENA)
    • Native RPC
  • OO Structures
  • Temporal Logic Assertions
  • Compiler Operation
    • Conversion to I-Code
    • Repeated Elaboration from each Entry Point until Closure
    • Compensation Path Determination
    • Compile Time Assertion Checking
    • Code Output
  • Model Checking
  • Bundle Meta Info
  • Binding Hooks
  
  
• Standard Environment
  • Bundle Meta Info
  • Local Variable Store
  • Pushlogic Timer
  • Assistance with Network Race Conditions
    • Test and Set Facility
    • Make/break Issues
  • Low-level Parallel Composition of Tuples.
  
  
• Plant Model
• Domain Manager
  • Using the compiler to check domains
  • Incremental and Real-time Model Checking
  • Federation of Pushlogic DoPs
  
  
• Pebbles and Pebble Formal Model
  • Platform Metainfo: Reflection via Pebble Dataplane
  • Bundle Metainfo: Reflection via Pebble Dataplane
  
  
• Execution Platforms
  • Registration
  • Code reflection
  • Web Interface
  • Pusher: Command Line and GUI Tool
    • Pusher Command Line Arguments
  • Console Output
  
  
• Other Issues
• Index
• Bibliography