Next:
Abstract
Contents
Index
Pushlogic SPL1
Language Reference Manual (draft).
Updated - January 2007
DJ Greaves
1
University of Cambridge, Computer Laboratory
Abstract
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
Event and Level Constraints
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
Elaboration of assignment
Elaboration of Sequential Composition
Elaboration of
WAIT
Elaboration of I
F/THEN/ELSE
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
About this document ...
David Greaves 2009-04-20
