使用人在回路合成来编写函数式反应程序
Using human-in-the-loop synthesis to author functional reactive programs
摘要：
响应异步事件的程序编写起来很有挑战性;它们很难推理，测试和调试也很棘手。因为这些程序可能有一个巨大的输入时间和交错空间，程序员可能很容易错过角落的情况。我们建议应用合成，以帮助程序员更容易地创建程序，并在其正确性有更高的信心。我们已经写了一个有效的编码的功能反应式编程（FRP）语义的基础上的功能编程在玫瑰解除列表。我们证明，这种技术是最先进的，首先比较其性能对现有的两个合成工具，产生列表操作程序，然后通过合成一套基准完整的规格。我们还提出了一个交互式工具，在该工具中，程序员以输入/输出示例或不变量的形式提供一些初始部分规范;该工具通过合成两个候选程序来发现规范中的歧义，并给用户一个区分它们的输入;用户更新规范并继续迭代直到找到正确的程序。作为评估，我们展示了使用该工具的一套基准测试，从网络编程和物联网领域，走查一个现实的网络基准测试的样本交互，表明我们可以收敛到目标程序与易处理的互动数量。作为未来的工作，我们讨论对其他FRP语言进行编码，以探索元语言特征、允许合成更大程序的分解策略以及改进的程序员工具（例如GUI），以更容易地得出规范。
英文摘要：
Programs that respond to asynchronous events are challenging to write; they are difficult to reason about and tricky to test and debug. Because these programs can have a huge space of possible input timings and interleaving, the programmer may easily miss corner cases. We propose applying synthesis to aid programmers in creating programs more easily and with a higher degree of confidence in their correctness. We have written an efficient encoding of functional reactive programming (FRP) semantics based on functional programming over lists lifted in Rosette. We demonstrate that this technique is state-of-the-art by first comparing its performance against two existing synthesis tools that produce list manipulation programs, and then by synthesizing a suite of benchmarks given complete specifications. We also propose an interactive tool in which a programmer provides some initial partial specification in the form of input/output examples or invariants; the tool finds ambiguity in the specification by synthesizing two candidate programs and gives the user an input that distinguishes them; the user updates the specification and continues iterating until the correct program is found. As evaluation, we demonstrate the use of the tool on a suite of benchmarks from the web programming and Internet of Things domains and walk through a sample interaction on a realistic web benchmark, showing that we can converge on the target program with a tractable number of interactions. As future work, we discuss encoding additional FRP languages to in order to explore metalinguistic features, strategies for decomposition that would allow the synthesis of larger programs, and improved programmer tools such as a GUI to more easily elicit specifications.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
