Projection semantics for rigid loops
arXiv:0707.1059
Abstract
A rigid loop is a for-loop with a counter not accessible to the loop body or any other part of a program. Special instructions for rigid loops are introduced on top of the syntax of the program algebra PGA. Two different semantic projections are provided and proven equivalent. One of these is taken to have definitional status on the basis of two criteria: `normative semantic adequacy' and `indicative algorithmic adequacy'.
20 pages
Cited by in corpus (18)
- Instruction sequences with indirect jumps
- Thread extraction for polyadic instruction sequences
- Instruction sequences and non-uniform complexity theory
- On the expressiveness of single-pass instruction sequences
- Tuplix Calculus Specifications of Financial Transfer Networks
- Transmission protocols for instruction streams
- Instruction sequences with dynamically instantiated instructions
- Instruction sequence notations with probabilistic instructions
- A process calculus with finitary comprehended terms
- Software (Re-)Engineering with PSF III: an IDE for PSF
- Programming an interpreter using molecular dynamics
- Meadow enriched ACP process algebras
- Software (Re-)Engineering with PSF II: from architecture to implementation
- On the operating unit size of load/store architectures
- Towards a formalization of budgets
- A process algebra based framework for promise theory
- A protocol for instruction stream processing
- Instruction sequences for the production of processes