Toward semantic search via SMT solver
Toward semantic search via SMT solver
复制标题
DOI：
10.1145/2393596.2393625
复制
发表时间：
2012-11
期刊：
影响因子：
--
通讯作者：
Kathryn T. Stolee;Sebastian G. Elbaum
中科院分区：
文献类型：
--
作者：
Kathryn T. Stolee;Sebastian G. Elbaum
搜索代码是程序员之间的常见任务，其最终重用目标是重复使用的目标。虽然搜索代码的过程（发布查询并选择相关匹配项）很简单，但必须平衡几个费用，包括指定查询的成本，检查结果以找到所需的代码，而找不到相关结果。对于句法搜索，查询成本很低，但是结果通常无关紧要，因此检查成本很高，可能会错过比赛。语义搜索可能会返回更多相关的结果，但是涉及编写复杂规格或针对测试用例执行代码的当前技术对开发人员来说是昂贵的。我们提出了一种语义搜索的方法，开发人员指定轻量级规格，而SMT求解器则标识了存储库中的匹配程序。程序存储库自动离线编码，因此搜索是有效的。程序以各种抽象级别进行编码，以启用不存在或很少有确切匹配的部分匹配。我们将这种方法实例化在Yahoo!的一部分上管道混搭语言。初步结果表明了该方法可行性的希望。
Searching for code is a common task among programmers, with the ultimate goal of reuse. While the process of searching for code -- issuing a query and selecting a relevant match -- is straightforward, several costs must be balanced, including the costs of specifying the query, examining the results to find desired code, and not finding a relevant result. For syntactic searches the query cost is quite low, but the results are often irrelevant, so the examination cost is high and matches may be missed. Semantic searches may return more relevant results, but current techniques that involve writing complex specifications or executing code against test cases are costly to the developer. We propose an approach for semantic search in which developers specify lightweight specifications and an SMT solver identifies matching programs from a repository. A program repository is automatically encoded offline so the search is efficient. Programs are encoded at various abstraction levels to enable partial matches when no, or few, exact matches exist. We instantiate this approach on a subset of the Yahoo! Pipes mashup language. Preliminary results show promise for the feasibility of the approach.