Laws of Parallel Synchronised Termination. Sands, D. 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 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
{"_id":"vGP3sbmpAZLDyFKxd","bibbaseid":"sands-lawsofparallelsynchronisedtermination-1993","downloads":0,"creationDate":"2017-02-03T08:24:26.847Z","title":"Laws of Parallel Synchronised Termination","author_short":["Sands, D."],"year":1993,"bibtype":"inproceedings","biburl":"http://www.cse.chalmers.se/~dave/davewww2016.bib","bibdata":{"bibtype":"inproceedings","type":"inproceedings","semno":"D-172","author":[{"firstnames":["David"],"propositions":[],"lastnames":["Sands"],"suffixes":[]}],"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":[{"firstnames":["G.L."],"propositions":[],"lastnames":["Burn"],"suffixes":[]},{"firstnames":["S.J."],"propositions":[],"lastnames":["Gay"],"suffixes":[]},{"firstnames":["M.D."],"propositions":[],"lastnames":["Ryan"],"suffixes":[]}],"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.","bibtex":"@INPROCEEDINGS{Sands:TFM,\n semno = {D-172},\n author = {David Sands},\n title = {Laws of Parallel Synchronised Termination},\n booktitle = {Theory and Formal Methods 1993: \n Proceedings of the First Imperial College, \n Department of Computing, \n Workshop on Theory and Formal Methods},\n editor = {G.L. Burn and S.J. Gay and M.D. Ryan},\n month = {March},\n year = {1993},\n address = {Isle of Thorns, UK},\n publisher = {Springer-Verlag},\n series = {Workshops in Computing Series},\n abstract = {The salient feature of the composition operators for \nGamma programs is that for termination, the parallel composition operator\ndemands that its operands must terminate synchronously. This paper studies\nthe inequational partial correctness properties of the combination of\nsequential and parallel composition operators for Gamma programs, provable\nfrom a particular compositional semantics (Brookes-style transition traces)\nand shows that the ``residual program'' input-output laws originally\ndescribed by Hankin {\\em et al.\\/} are also verified by the model.},\n}\n\n","author_short":["Sands, D."],"editor_short":["Burn, G.","Gay, S.","Ryan, M."],"key":"Sands:TFM","id":"Sands:TFM","bibbaseid":"sands-lawsofparallelsynchronisedtermination-1993","role":"author","urls":{},"downloads":0},"search_terms":["laws","parallel","synchronised","termination","sands"],"keywords":[],"authorIDs":["58943e3a2f18920f4c000022"],"dataSources":["SBHWXKotbthoEYKJv"]}