{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T12:00:26Z","timestamp":1762862426630},"reference-count":31,"publisher":"Elsevier BV","issue":"2-3","license":[{"start":{"date-parts":[[1994,12,1]],"date-time":"1994-12-01T00:00:00Z","timestamp":786240000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":6803,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[1994,12]]},"DOI":"10.1016\/0167-6423(94)00017-4","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T04:09:22Z","timestamp":1027656562000},"page":"107-125","source":"Crossref","is-referenced-by-count":13,"title":["Composition of assumption-commitment specifications in a UNITY style"],"prefix":"10.1016","volume":"23","author":[{"given":"Pierre","family":"Collette","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0167-6423(94)00017-4_BIB1","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","article-title":"The existence of refinement mappings","volume":"82","author":"Abadi","year":"1991","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0167-6423(94)00017-4_BIB2","series-title":"Real Time: Theory in Practice","first-page":"1","article-title":"An old-fashioned recipe for real time","volume":"600","author":"Abadi","year":"1992"},{"key":"10.1016\/0167-6423(94)00017-4_BIB3","doi-asserted-by":"crossref","unstructured":"M. aBADI and L. Lamport, Composing specifications, ACM Trans. Prog. Langauges Systems 15 73\u2013132.","DOI":"10.1145\/151646.151649"},{"key":"10.1016\/0167-6423(94)00017-4_BIB4","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(93)90151-I","article-title":"A logical view of composition","volume":"114","author":"Abadi","year":"1993","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0167-6423(94)00017-4_BIB5","series-title":"On an inference rule for parallel composition","author":"Aczel","year":"1983"},{"key":"10.1016\/0167-6423(94)00017-4_BIB6","first-page":"51","article-title":"Now you may compose temporal logic specifications","author":"Barringer","year":"1984","journal-title":"Proceedings of the 16th ACM Symposium on Theory of Computing"},{"key":"10.1016\/0167-6423(94)00017-4_BIB7","series-title":"Parallel Program Design: a Foundation","author":"Chandy","year":"1988"},{"key":"10.1016\/0167-6423(94)00017-4_BIB8","series-title":"Proceedings of TAPSOFT'93: Theory and Practice of Software Development","first-page":"230","article-title":"Application of the composition principle to Unity-like specifications","volume":"668","author":"Collette","year":"1993"},{"key":"10.1016\/0167-6423(94)00017-4_BIB9","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/0020-0190(94)90041-8","article-title":"An explanatory presentation of composition rules for assumption-commitment specifications","volume":"50","author":"Collette","year":"1994","journal-title":"Inform. Process. Lett."},{"key":"10.1016\/0167-6423(94)00017-4_BIB10","series-title":"Technical Report","article-title":"A compositional proof system for UNITY based on rely\/guarantee conditions","author":"Collette","year":"1993"},{"key":"10.1016\/0167-6423(94)00017-4_BIB11","series-title":"Formal Models of Programming","first-page":"181","article-title":"The quest for compositionality\u2014a survey of assertion based proof systems for concurrent programs, part I","author":"de Roever","year":"1987"},{"key":"10.1016\/0167-6423(94)00017-4_BIB12","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/BF01212304","article-title":"Temporal theories as modularisation units for concurrent system specification","volume":"4","author":"Fiadeiro","year":"1992","journal-title":"Formal Aspects Comput."},{"key":"10.1016\/0167-6423(94)00017-4_BIB13","series-title":"Foundations of Software Technology and Theoretical Computer Science","first-page":"332","article-title":"Refinement and composition of transition-based rely-guarantee specifications with auxiliary variables","volume":"472","author":"Gr\u2205nning","year":"1991"},{"key":"10.1016\/0167-6423(94)00017-4_BIB14","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1145\/69575.69577","article-title":"Tentative steps towards a development method for interfering programs","volume":"5","author":"Jones","year":"1983","journal-title":"ACM Trans. Programming Languages Systems"},{"key":"10.1016\/0167-6423(94)00017-4_BIB15","series-title":"FME'93: Industrial Strength Formal Methods","first-page":"1","article-title":"Reasoning about interference in an object-based design method","volume":"670","author":"Jones","year":"1993"},{"key":"10.1016\/0167-6423(94)00017-4_BIB16","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0167-6423(92)90002-S","article-title":"Derivation of concurrent programs: two examples","volume":"19","author":"Knapp","year":"1992","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/0167-6423(94)00017-4_BIB17","doi-asserted-by":"crossref","unstructured":"L. Lamport, The temporal logic of actions, ACM Trans. Prog. Languages Systems 16 872-923.","DOI":"10.1145\/177492.177726"},{"key":"10.1016\/0167-6423(94)00017-4_BIB18","series-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Manna","year":"1992"},{"key":"10.1016\/0167-6423(94)00017-4_BIB19","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1109\/TSE.1981.230844","article-title":"Proofs of networks of processes","volume":"7","author":"Misra","year":"1981","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/0167-6423(94)00017-4_BIB20","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/0167-6423(90)90019-A","article-title":"Specifying concurrent objects as communicating processes","volume":"14","author":"Misra","year":"1990","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/0167-6423(94)00017-4_BIB21","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/BF02311231","article-title":"P-A logic\u2014a compositional proof system for distributed programs","volume":"5","author":"Pandya","year":"1991","journal-title":"Distrib. Comput."},{"key":"10.1016\/0167-6423(94)00017-4_BIB22","series-title":"Research Directions in High-Level Parallel Programming Languages","first-page":"39","article-title":"An industrial experience in the use of Unity","volume":"574","author":"Pizzarello","year":"1991"},{"key":"10.1016\/0167-6423(94)00017-4_BIB23","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/BF01898402","article-title":"Eliminating the substitution axiom from Unity logic","volume":"3","author":"Sanders","year":"1991","journal-title":"Formal Aspects Comput."},{"key":"10.1016\/0167-6423(94)00017-4_BIB24","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/0167-6423(91)90023-Q","article-title":"Specification of concurrent objects using auxiliary variables","volume":"16","author":"Singh","year":"1991","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/0167-6423(94)00017-4_BIB25","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(86)90007-1","article-title":"Proving entailment between conceptual state specifications","volume":"56","author":"Stark","year":"1988","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0167-6423(94)00017-4_BIB26","series-title":"Proceedings of Concur'91","first-page":"510","article-title":"A method for the development of totally correct shared-state parallel programs","volume":"527","author":"St\u2205len","year":"1991"},{"key":"10.1016\/0167-6423(94)00017-4_BIB27","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1109\/32.232015","article-title":"Formal derivation of concurrent programs: an example from industry","volume":"19","author":"Staskauskas","year":"1993","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/0167-6423(94)00017-4_BIB28","series-title":"Semantics: Foundations and Applications","first-page":"594","article-title":"On the relation between Unity properties and sequences of states","volume":"666","author":"Udink","year":"1993"},{"key":"10.1016\/0167-6423(94)00017-4_BIB29","series-title":"Proceedings of VDM'88: The Way Ahead","first-page":"434","article-title":"Using VDM with rely and guarantee-conditions","volume":"328","author":"Woodcock","year":"1988"},{"key":"10.1016\/0167-6423(94)00017-4_BIB30","series-title":"Proceedings of the 4th BCS-FACS Refinement Workshop","first-page":"326","article-title":"A theory of state-based parallel programming: part I","author":"Xu","year":"1991"},{"key":"10.1016\/0167-6423(94)00017-4_BIB31","article-title":"Compositionality, Concurrency and Partial Correctness","volume":"321","author":"Zwiers","year":"1989"}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0167642394000174?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0167642394000174?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,2,5]],"date-time":"2020-02-05T13:33:51Z","timestamp":1580909631000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0167642394000174"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,12]]},"references-count":31,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[1994,12]]}},"alternative-id":["0167642394000174"],"URL":"https:\/\/doi.org\/10.1016\/0167-6423(94)00017-4","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[1994,12]]}}}