arrow
返回

Software Synthesis Procedures

delete2012-02-01
delete23
delete
OA
AI
V
Viktor Kunčak *
M
Mikaël Mayer
R
Ružica Piskač
P
Philippe Suter
DOI:10.1145/2076450.2076472delete
delete原文链接
delete分享
delete收藏
查看原文
摘要

摘要

En 中文
Automated synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, software synthesis algorithms should behave in a predictable way: they should succeed for a well-defined class of specifications. We propose to systematically generalize decision procedures into synthesis procedures, and use them to compile implicitly specified computations embedded inside functional and imperative programs. Synthesis procedures are predictable, because they are guaranteed to find code that satisfies the specification whenever such code exists. To illustrate our method, we derive synthesis procedures by extending quantifier elimination algorithms for integer arithmetic and set data structures. We then show that an implementation of such synthesis procedures can extend a compiler to support implicit value definitions and advanced pattern matching.
Keyword:
PRACTICAL ALGORITHM
AI总结

AI总结

对已上传原文的论文进行重点信息的提取,主要内容包括:简要概述、研究摘要、背景介绍、关键亮点、图文解析、展望与总结。

期刊

Communications of the ACM 封面图
Communications of the ACM
IF:
12.2
论文数:
1.2W
被引数:
3.7W

机构

S
swiss federal institutes of technology domain
学者数:
795
论文数: 1.1K
被引数: 0
引用论文

引用论文

err分享
err收藏
err分享
err收藏
Melatonin Alleviates Contrast‐Induced Acute Kidney Injury by Activation of Sirt3
err2021-05-25
err0
errOAAI
errChunmei Zhang; Mengying Suo; Lingxin Liu; Yan Qi; Chen Zhang; Lin Xie; Xuehui Zheng; Chang Ma; Jingyuan Li; Jianmin Yang; Peili Bu
err分享
err收藏
Lithiation of 1-phenylsulfenyl-4-penten-1-ynes and reactions with electrophiles
err1993-01-01
err0
PREAI
errSaverio Florio; Ludovico Ronzini; Erbana Epifani; Riccardo Sgarra
err分享
err收藏
err分享
err收藏
学者 查看更多内容