This paper introduces a programming construct--DOupon--that is a semantic generalization of the alternative and iterative constructs. The main motivation, as stated by the author, is that DOupon “provides more expressive power and simplifies the synthesis and proofs of algorithms.”

The author defines Hoare-like semantics of DOupon statements and presents theorems for the total and partial correctness proofs. Because the construct is nondeterministic, theorems are provided to guide the optimization of DOupon statements while preserving their correctness.

As specified by the author, Parnas has proposed a very similar construct [1]. The main difference between the two papers lies in the formalisms used: Hoare logic by Anson and set theory by Parnas. Coming four years after [1], Anson’s paper does not bring any fundamentally new ideas. On the other hand, I found the optimization transformations rather attractive and of practical interest.