Process expressions and Hoare's logic: Showing and irreconcilability of context-free recursion with Scott's induction rule (Q1183608)

A non-uniform process specification language is presented. It contains constants for a set of atomic actions, constructs for alternative and sequential composition and recursion. Processes are considered as having a state in the sense that atomic actions are to be specified in terms of observable behaviour (relative to initial states) and state transformations. An operational semantics is given in the style of Plotkin. The process having an initial state is associated with a transition system representing all possible courses of execution. An execution of an atomic action \(a\) in a state \(s\) is specified by functions \(action\) and \textit{affect}. The expression \(action (a,s)\) denotes what can be observed if \(a\) is executed in state \(s\) and the expression \textit{affect}\((a,s)\) denotes the resulting state. A partial correctness assertion \(\{\alpha\}p\{\beta\}\) is introduced. It expresses that for any transition system associated with \(p\) having an initial state satisfying \(\alpha\), its final states representing a successful execution satisfying \(\beta\). Hoare's logic containing a proof system for deriving partial correctness assertions is presented. The proof system is sound and relatively complete. It is shown by example that the completeness of the logic is lost if pure recursion is replaced by guarded recursion in the language.