Program logics typically reason about an over-approximation of program behaviour to prove the absence of bugs. Recently, program logics have been proposed that instead prove the presence of bugs by means of under-approximate reasoning, which has the promise of better scalability. In this paper, we present an under-approximate program logic for a nondeterministic graph programming language, and show how it can be used to reason deductively about program incorrectness, whether defined by the presence of forbidden graph structure or by finitely failing executions. We prove this incorrectness logic to be sound and complete, and speculate on some possible future applications of it.
翻译:程序逻辑通常说明程序行为过度偏好的理由,以证明没有错误。 最近,有人提议程序逻辑,以近似推理来证明存在错误,这有可能改善可缩放性。 在本文中,我们提出了一个非确定性图表编程语言的近似程序逻辑,并表明如何利用它来推算程序不正确性,无论是用被禁止的图表结构来界定,还是用有限的不成功处决来界定。 我们证明这种不正确逻辑是正确和完整的,并推测它今后可能使用的某些用途。