摘要: Another way in which the level of abstraction can change development is through granularity operations, particular changing one abstract operation into several concrete ones. This chapter considers consequences allowing operations to be decomposed refinement, involves further generalisation theory from Chap. 3. often known as non-atomic or action refinement literature. The final sections discuss applications verifying concurrent data structures.
springer.com
sci-hub.st 参考文章(31)
Kaisa Sere, Marina Waldén, Data Refinement of Remote Procedures Formal Aspects of Computing. ,vol. 12, pp. 278- 297 ,(2000) , 10.1007/PL00003935
Robert Colvin, Simon Doherty, Lindsay Groves, Verifying Concurrent Data Structures by Simulation Electronic Notes in Theoretical Computer Science. ,vol. 137, pp. 93- 110 ,(2005) , 10.1016/J.ENTCS.2005.04.026
Richard J. Lipton, Reduction Communications of the ACM. ,vol. 18, pp. 717- 721 ,(1975) , 10.1145/361227.361234
John Derrick, Gerhard Schellhorn, Heike Wehrheim, Mechanically verified proof obligations for linearizability ACM Transactions on Programming Languages and Systems. ,vol. 33, pp. 1- 43 ,(2011) , 10.1145/1889997.1890001
Maurice P. Herlihy, Jeannette M. Wing, Linearizability: a correctness condition for concurrent objects ACM Transactions on Programming Languages and Systems. ,vol. 12, pp. 463- 492 ,(1990) , 10.1145/78969.78972
John Derrick, Gerhard Schellhorn, Heike Wehrheim, Proving Linearizability Via Non-atomic Refinement Lecture Notes in Computer Science. pp. 195- 214 ,(2007) , 10.1007/978-3-540-73210-5_11
Cátia Vaz, Carla Ferreira, On the analysis of compensation correctness The Journal of Logic and Algebraic Programming. ,vol. 81, pp. 585- 605 ,(2012) , 10.1016/J.JLAP.2012.04.002
Matthew Parkinson, Richard Bornat, Peter O'Hearn, Modular verification of a non-blocking stack symposium on principles of programming languages. ,vol. 42, pp. 297- 302 ,(2007) , 10.1145/1190215.1190261
Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, Marc Shapiro, Proving correctness of highly-concurrent linearisable objects acm sigplan symposium on principles and practice of parallel programming. pp. 129- 136 ,(2006) , 10.1145/1122971.1122992
Martin Vechev, Eran Yahav, Deriving linearizable fine-grained concurrent objects Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation - PLDI '08. ,vol. 43, pp. 125- 135 ,(2008) , 10.1145/1375581.1375598