A Functional Calculus for Specification and Verification of Nondeterministic Interactive Systems

We introduce a language in terms of syntax and a logical calculus that provides a theory for the specification and logical deduction of functional and relational programs modeling nondeterministic interactive systems specifications. We use formulas of classical predicate logic for formulating the specifications. The calculus consists of special rules for manipulating these formulas. These rules allow us to transform formulas containing functional nondeterministic programs into pure formulas of predicate logic. We put emphasis onto rules for the treatment of nondeterminism and recursive declarations including communication feedback. This way both a design calculus for the transformational development of interactive functional programs, as well as a calculus for their verification, is given. We demonstrate the usage of the calculus by a number of short examples.