2007/07/06 by J.A. Bergstra, Bergstra, Jan A., Alban Ponse +1 · 2 citations
Computer Science · #D.2.4 #D.3.1 #F.3.2 #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.0707.1059
openalex publication_date 2007/07/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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'.