%0 Journal Article %1 Abadi:1993:CS:151646.151649 %A Abadi, Mart\'ın %A Lamport, Leslie %C New York, NY, USA %D 1993 %I ACM %J ACM Trans. Program. Lang. Syst. %K composition compositionality concurrent_programming consistency modular_specification %P 73--132 %R 10.1145/151646.151649 %T Composing specifications %U http://doi.acm.org/10.1145/151646.151649 %V 15 %X <par>A rigorous modular specification method requires a proof rule asserting that if each component behaves correctly in isolation, then it behaves correctly in concert with other components. Such a rule is subtle because a component need behave correctly only when its environment does, and each component is part of the others' environments. We examine the precise distinction between a system and its environment, and provide the requisite proof rule when modules are specified with safety and liveness properties.</par>

@article{Abadi:1993:CS:151646.151649, abstract = {<par>A rigorous modular specification method requires a proof rule asserting that if each component behaves correctly in isolation, then it behaves correctly in concert with other components. Such a rule is subtle because a component need behave correctly only when its environment does, and each component is part of the others' environments. We examine the precise distinction between a system and its environment, and provide the requisite proof rule when modules are specified with safety and liveness properties.</par>}, acmid = {151649}, added-at = {2011-12-16T09:27:31.000+0100}, address = {New York, NY, USA}, author = {Abadi, Mart\'{\i}n and Lamport, Leslie}, biburl = {https://www.bibsonomy.org/bibtex/2c94c826a2f211d29bd8bcf32cb838a2a/pbrada}, doi = {10.1145/151646.151649}, interhash = {0832de602b4f81ceae78d937e16a2b3c}, intrahash = {c94c826a2f211d29bd8bcf32cb838a2a}, issn = {0164-0925}, issue = {1}, journal = {ACM Trans. Program. Lang. Syst.}, keywords = {composition compositionality concurrent_programming consistency modular_specification}, month = {January}, numpages = {60}, pages = {73--132}, publisher = {ACM}, timestamp = {2011-12-16T09:27:31.000+0100}, title = {Composing specifications}, url = {http://doi.acm.org/10.1145/151646.151649}, volume = 15, year = 1993 }