Predicative semantics of loops

A predicative semantics is a mapping of programs to predicates. These predicates characterize sets of acceptable observations. The presence of time in the observations makes the obvious weakest xed-point semantics of iterative constructs unacceptable. This paper proposes an alternative. We will see that this alternative semantics is monotone and implementable (feasible). Finally a programming theorem for iterative constructs is proposed, proved, and demonstrated. A novel aspect of this theorem is that it is not based on invariants. Keywords Predicative semantics, xedpoint semantics, recursion, loops, re nement calculi. 0 FORMALIZATION 0.0 Speci cations and re nement De ne xnat as the set of all natural numbers (nat) joined with an additional

• Type: Conference
• Year: 1997
• Where: ALC
• Authors: Theodore S. Norvell
• Keywords: ALC 1997, Iterative Constructs, Predicative Semantics, Programming Languages, Weakest Xed-point Semantics