Program Extrapolation with Jennisys
Program Extrapolation with Jennisys
复制标题
DOI：
10.1145/2398857.2384646
复制
发表时间：
2012-10-01
影响因子：
--
通讯作者：
Milicevic, Aleksandar
中科院分区：
文献类型：
--
作者：
Leino, K. Rustan M.;Milicevic, Aleksandar
可以使用抽象模型来描述程序的所需行为。将这种模型编译到可执行的代码中需要高级编译技术称为合成。本文介绍了一种基于对象的语言，称为Jennisys，在其中通过引入抽象模型，定义模型的具体数据表示来完成编程，然后通过自动合成以生成可执行代码的帮助。本文还提出了该语言的合成技术。该技术建立在自动程序验证器上，通过基础SMT求解器，该验证者能够为失败的验证提供具体的模型。该技术通过从混凝土模型中获取样品输入/输出值，然后从样本点外推程序来进行。该综合旨在通过分配，分支结构以及可能的递归调用生成代码。它是第一个合成在动态数据结构或聚合对象中创建和使用对象的代码的代码。已经实施了语言和综合技术的原型。
The desired behavior of a program can be described using an abstract model. Compiling such a model into executable code requires advanced compilation techniques known as synthesis. This paper presents an object-based language, called Jennisys, where programming is done by introducing an abstract model, defining a concrete data representation for the model, and then being aided by automatic synthesis to produce executable code. The paper also presents a synthesis technique for the language. The technique is built on an automatic program verifier that, via an underlying SMT solver, is capable of providing concrete models to failed verifications. The technique proceeds by obtaining sample input/output values from concrete models and then extrapolating programs from the sample points. The synthesis aims to produce code with assignments, branching structure, and possibly recursive calls. It is the first to synthesize code that creates and uses objects in dynamic data structures or aggregate objects. A prototype of the language and synthesis technique has been implemented.