In Burn, G., Gay, S., & Ryan, M., editors, *Theory and Formal Methods 1993: Proceedings of the First Imperial College, Department of Computing, Workshop on Theory and Formal Methods*, of *Workshops in Computing Series*, Isle of Thorns, UK, March, 1993. Springer-Verlag.

abstract bibtex

abstract bibtex

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'' input-output laws originally described by Hankin \em et al.\/ are also verified by the model.

@INPROCEEDINGS{Sands:TFM, semno = {D-172}, author = {David Sands}, title = {Laws of Parallel Synchronised Termination}, booktitle = {Theory and Formal Methods 1993: Proceedings of the First Imperial College, Department of Computing, Workshop on Theory and Formal Methods}, editor = {G.L. Burn and S.J. Gay and M.D. Ryan}, month = {March}, year = {1993}, address = {Isle of Thorns, UK}, publisher = {Springer-Verlag}, series = {Workshops in Computing Series}, abstract = {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'' input-output laws originally described by Hankin {\em et al.\/} are also verified by the model.}, }

Downloads: 0