论文标题
不实现的逻辑
Unrealizability Logic
论文作者
论文摘要
我们认为确定程序合成问题是无法实现的问题（即，在给定的程序的搜索空间中没有解决方案）。先前的关于不实现性的工作已经开发出一些自动技术，以确定问题是无法实现的。但是，这些技术都是黑框，这意味着它们掩盖了为什么综合问题无法实现的背后推理。在本文中，我们提出了一个hoare式的推理系统，称为不实现程序合成问题是无法实现的。据我们所知，不实现的逻辑是过度应用无限命令程序的第一个证明系统。该逻辑提供了一个通用的逻辑系统，用于构建有关不实现性的可检查证明。类似于Hoare逻辑如何提炼算法和工具背后的基本概念以证明程序的正确性，不实现的逻辑蒸馏涉及单个逻辑系统，隐藏在先验工具中的基本概念能够确定程序合成问题是无法实现的。
We consider the problem of establishing that a program-synthesis problem is unrealizable (i.e., has no solution in a given search space of programs). Prior work on unrealizability has developed some automatic techniques to establish that a problem is unrealizable; however, these techniques are all black-box, meaning that they conceal the reasoning behind why a synthesis problem is unrealizable. In this paper, we present a Hoare-style reasoning system, called unrealizability logic for establishing that a program-synthesis problem is unrealizable. To the best of our knowledge, unrealizability logic is the first proof system for overapproximating the execution of an infinite set of imperative programs. The logic provides a general, logical system for building checkable proofs about unrealizability. Similar to how Hoare logic distills the fundamental concepts behind algorithms and tools to prove the correctness of programs, unrealizability logic distills into a single logical system the fundamental concepts that were hidden within prior tools capable of establishing that a program-synthesis problem is unrealizable.
