Unifying execution of imperative generators and declarative specifications
Unifying execution of imperative generators and declarative specifications
复制标题
统一命令式生成器和声明性规范的执行
DOI：
10.1145/3428285
复制
发表时间：
2020
影响因子：
--
通讯作者：
Gligoric, Milos
中科院分区：
文献类型：
--
作者：
Nie, Pengyu;Parovic, Marinela;Zang, Zhiqiang;Khurshid, Sarfraz;Milicevic, Aleksandar;Gligoric, Milos
我们提出了氘---一个框架实现Java方法作为可执行的合同。Deuterium引入了一种新颖的类型安全的方式来完全用Java编写方法契约，作为命令式生成器和声明式规范的组合（用一阶关系逻辑和传递闭包编写）。现有的方法通常基于将规范和程序堆编码成约束语言，然后使用现成的约束求解器-没有任何额外的指导-来搜索满足规范的新程序堆。氘利用用户提供的生成器修剪搜索空间，减少约束求解的开销。氘支持两种解决声明性约束的方法：基于SAT和基于搜索的内存状态探索。我们评估我们的方法上的一套数据结构，建立了一个标准的基准，由以前的工作。此外，我们使用随机和基于序列的测试生成来创建旨在模拟现实执行场景的新基准。我们的研究结果表明，发电机提高了可执行合同的性能，内存中的状态探索是堆大小小时的选择算法。
We present Deuterium---a framework for implementing Java methods as executable contracts. Deuterium introduces a novel, type-safe way to write method contracts entirely in Java, as a combination of imperative generators and declarative specifications (written in a first-order relational logic with transitive closure). Existing approaches are typically based on encoding both the specification and the program heap into a constraint language, and then using an off-the-shelf constraint solver---without any additional guidance---to search for a new program heap that satisfies the specification. Deuterium takes advantage of user-provided generators to prune the search space and reduce incurred overhead of constraint solving. Deuterium supports two ways of solving declarative constraints: SAT-based and search-based with in-memory state exploration. We evaluate our approach on a suite of data structures, established as a standard benchmark by prior work. Furthermore, we use random and sequence-based test generation to create a new benchmark designed to mimic realistic execution scenarios. Our results show that generators improve the performance of executable contracts and that in-memory state exploration is the algorithm of choice when heap sizes are small.
登录
查看更多内容
做出随机判断：根据类型系统的定义自动生成类型良好的术语
DOI：
--
发表时间：
2015
期刊：
European Symposium on Programming
影响因子：
--
作者：
B. Fetscher;Koen Claessen;Michal H. Palka;John Hughes;R. Findler
通讯作者：
R. Findler
万花筒：一种约束命令式编程语言
DOI：
10.1007/978-3-642-85983-0_12
发表时间：
1993
期刊：
IEEE INFOCOM 2021 - IEEE Conference on Computer Communications Workshops (INFOCOM WKSHPS)
影响因子：
--
作者：
Gus Lopez;B. Freeman;A. Borning
通讯作者：
A. Borning
将一组合同检查工具集成到 Visual Studio 中
DOI：
10.1109/topi.2012.6229809
发表时间：
2012
期刊：
2012 Second International Workshop on Developing Tools as Plug-Ins (TOPI)
影响因子：
--
作者：
M. Fähndrich;Mike Barnett;Daan Leijen;F. Logozzo
通讯作者：
F. Logozzo
影响因子：
--
作者：
F. Logozzo
通讯作者：
F. Logozzo
Astra 版本 1.0：评估从合金到 SMT-LIB 的翻译
DOI：
10.1007/978-3-662-46675-9_20
发表时间：
2019
期刊：
ArXiv
影响因子：
--
作者：
Ali Abbassi;N. Day;Derek Rayside
通讯作者：
Derek Rayside