Projection semantics for rigid loops

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 (8)

• Instruction sequences with indirect jumps
• Tuplix Calculus Specifications of Financial Transfer Networks
• Programming an interpreter using molecular dynamics
• Software (Re-)Engineering with PSF III: an IDE for PSF
• Software (Re-)Engineering with PSF II: from architecture to implementation
• Towards a formalization of budgets
• A process algebra based framework for promise theory
• Instruction sequences for the production of processes