一句话:提出持续推理,将形式化推理融入持续迭代的代码库开发,以扩展形式化方法的适用范围。
本文讨论“持续推理”,即针对不断变化的代码库进行形式化推理,使其与工业界日益采用的迭代式、持续化软件开发模式相呼应。作者阐述持续推理的动机:传统形式化方法难以随代码演进和程序员规模而扩展,而持续开发需要持续的分析与推理。论文总结工业界的若干成功案例,并提出科学界可推进的研究方向,目标在于让形式化推理扩展到更多程序和更多程序员。
This paper describes work in continuous reasoning, where formal reasoning about a (changing) codebase is done in a fashion which mirrors the iterative, continuous model of software development that is increasingly practiced in industry. We suggest that advances in continuous reasoning will allow formal reasoning to scale to more programs, and more programmers. The paper describes the rationale for continuous reasoning, outlines some success cases from within industry, and proposes directions for work by the scientific community.