Refinement Semantics and Loop Rules

Refinement semantics is an alternative to least fixpoint semantics that is more useful for programming. From it we derive a variety of rules for w h i l e-loops, for-loops, and loops with intermediate and deep exits. We illustrate the use of these rules with examples. © Springer-Verlag 1999. to appear in LNCS for FM'99

• Type: Conference
• Year: 1999
• Where: FM
• Authors: Eric C. R. Hehner, Andrew M. Gravell
• Keywords: Deep Exits, Fixpoint Semantics, FM 1999, Formal Methods, Refinement Semantics