Semantic models for total correctness and fairness (Q1208419)

The purpose of this well-written paper is to provide a framework in which tools from linear algebra can be used to reason about the control structures of iterative nondeterministic programs. The results of the paper expand on some ideas of \textit{E. Manes} [Lect. Notes Comput. Sci. 298, 85-120 (1980; Zbl 0678.68082)] by adding a treatment of nontermination and fairness. Nondeterministic programs denote elements in certain structures, the \(s\)- rings, \((S,+,\cdot,0,1)\) which are almost semirings - the law \(s0=0\) need not hold. The prime example of such \(s\)-rings are the strict binary relations \(s\) on a set \(D\cup \{\perp\}\), i.e., those satisfying \((\perp,x)\in s\) iff \(x={\perp}\). The relational composition provides the multiplication, and union is the additon; the 0-element contains the single pair \((\perp,\perp)\); the identity relation is 1. The elements in the set \(D\) are `states' and the element \(\perp\) represents nontermination. The \(s\)-rings are expanded by two unary operations, written \(s^*\) and \(S^ \infty\). In the \(s\)-ring of relations, \(s^*\) represents reflexive transitive closure of \(s\); the relation \(s^ \infty\) contains exactly those pairs \((x,\perp)\) such that there is an infinite sequence \((x_ n:n\geq0)\) such that \(x=x_ 0\) and \((x_ ,x_{i+1})\in s\), for all \(i\). It is shown how to represent guards in any zero-sum-free \(s\)-ring, and it is shown why they form a boolean algebra. In the relational example, the guards the subrelations of the identity, i.e., \((x,y)\in p\Rightarrow y=x\). Among others, two infinitary axioms are assumed. \(\forall i\geq 0(rs^ it=0)\Rightarrow rs^*t=0\), \(\bigvee W\) exists and \(\forall p\in W(ps=0)\Rightarrow (\bigvee W)s=0\). When \(p,q\) are guards, the total correctness assertion \([p]s[q]\) is defined to mean that \(p\bar sq=0\), where \(\bar q\) is the complement in the boolean algebra of guards. (It is easily seen that in the relational example, this definition captures the standard defintion: if \(x\) is a state satisfying the guard \(p\), then the relation \(s\) is defined on \(x\) and if \((x,y)\in s\), \(y\) satisfies \(q\).) Rules are given to prove correctness assertions of the form: \([p]st[q],[p]s+t[q],[p]s^*[q],[p]s^ \infty[q]\). Under certain assumptions (the guards form a complete boolean algebra, and others), the rules given are shown complete. Those interested in algebraic treatments of correctness logic should see also the paper by the reviewer and \textit{Z. Ésik} [Proceedings of Mathematical Foundations of Programming Semantics 1991, Lect. Notes Comput. Sci. 598, 457-475 (1991)]. Although the setting is different, it includes the example of strict relations. From assumptions only about the finitary equational properties of iteration, the existence of both of the unary operations \(s^*\), \(s^ \infty\) is derived, as well as the equational properties of the guards; a necessary and sufficient condition, the ``invariant guard property'' is given for the completeness of the Floyd-Hoare partial correctness rules. Further, the rules also apply to matrices.