Semantic models for total correctness and fairness

AbstractAssertional s-rings are introduced to provide an algebraic setting in which the finite and infinite behavior of nondeterministic programs can be expressed and reasoned about. This includes expressing the fair infinite behavior of nondeterministic iterative programs, and reasoning about termination under various fairness assumptions. We also address the question of when the reasoning techniques are semantically complete