Laws of Parallel Synchronised Termination

The salient feature of the composition operators for Gamma programs is that for termination, the parallel composition operator demands that its operands must terminate synchronously. This paper studies the inequational partial correctness properties of the combination of sequential and parallel composition operators for Gamma programs, provable from a particular compositional semantics (Brookes-style transition traces) and shows that the “residual program” inputoutput laws originally described by Hankin et al. are also verified by the model.

• Type: Conference
• Year: 1993
• Where: IMPERIAL
• Authors: David Sands
• Keywords: Composition Operators, Formal Methods, Gamma Programs, IMPERIAL 1993, Parallel Composition Operators