caa a22 4500 605516197 CHVBK 20210128100713.0 cr unu---uuuuu 210128e20150501xx s 000 0 eng 10.1007/s00165-014-0322-y doi (NATIONALLICENCE)springer-10.1007/s00165-014-0322-y Compositional reasoning about active objects with shared futures [Elektronische Daten] [Crystal Din, Olaf Owe] Distributed and concurrent object-oriented systems are difficult to analyze due to the complexity of their concurrency, communication, and synchronization mechanisms. The future mechanism extends the traditional method call communication model by facilitating sharing of references to futures. By assigning method call result values to futures, third party objects may pick up these values. This may reduce the time spent waiting for replies in a distributed environment. However, futures add a level of complexity to program analysis, as the program semantics becomes more involved. This paper presents a model for asynchronously communicating objects, where return values from method calls are handled by futures. The model facilitates invariant specifications over the locally visible communication history of each object. Compositional reasoning is supported and proved sound, as each object may be specified and verified independently of its environment. A kernel object-oriented language with futures inspired by the ABS modeling language is considered. A compositional proof system for this language is presented, formulated within dynamic logic. British Computer Society, 2014 Distributed systems nationallicence Object orientation nationallicence Concurrent objects nationallicence Asynchronous communication nationallicence Shared futures nationallicence Operational semantics nationallicence Communication history nationallicence Compositional reasoning nationallicence Dynamic logic nationallicence Din Crystal Department of Computer Science, Technische Universität Darmstadt, Darmstadt, Germany aut Owe Olaf Department of Informatics, University of Oslo, Oslo, Norway aut Formal Aspects of Computing Springer London 27/3(2015-05-01), 551-572 0934-5043 27:3<551 2015 27 165 https://doi.org/10.1007/s00165-014-0322-y text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-014-0322-y text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Din Crystal Department of Computer Science, Technische Universität Darmstadt, Darmstadt, Germany aut NATIONALLICENCE 700 1- Owe Olaf Department of Informatics, University of Oslo, Oslo, Norway aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/3(2015-05-01), 551-572 0934-5043 27:3<551 2015 27 165