Software Engineering and Formal Methods - 13th International Conference, SEFM 2015, York, UK, September 7-11, 2015. Proceedings
Software Engineering and Formal Methods - 13th International Conference, SEFM 2015, York, UK, September 7-11, 2015. Proceedings
复制标题
软件工程和形式化方法 - 第 13 届国际会议，SEFM 2015，英国约克，2015 年 9 月 7-11 日。会议记录
DOI：
10.1007/978-3-319-22969-0_1
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Jones C
中科院分区：
文献类型：
--
作者：
Jones C
显示并发线程在其共享状态的不同部分上操作是建立非干扰的一种方法。此外，在许多有用的程序中，状态部分的所有权是动态交换的。关于基于堆的变量的分离和所有权的推理通常使用某种形式的分离逻辑进行。本文探讨了分离的问题，并研究了使用抽象来指定和推理程序设计中的分离。两个案例研究表明，使用分离作为一个抽象是一个潜在的有用的方法。
Showing that concurrent threads operate on separate portions of their shared state is a way of establishing non-interference. Furthermore, in many useful programs, ownership of parts of the state are exchanged dynamically. Reasoning about separation and ownership of heap-based variables is often conducted using some form of separation logic. This paper examines theissue of separationand investigates the use of abstraction to specify and to reason about separation in program design. Two case studies demonstrate that usingseparation as an abstractionis a potentially useful approach.