Incrementality is a fundamental design principle to master the complexity of large, long-lived software systems. This principle has been embraced by agile development processes and it lays at the base of continuous software evolution. A major challenge in this context is to incrementally re-verify the correctness of software artifacts after every change, focusing the verification efforts only on the parts affected by the change. We present an approach to the incremental verification of programs written in KernelC, annotated with properties expressed in matching logic. The approach is based on a syntactic-semantic framework that enables analyzing code chunks in isolation so that, after a change to a program fragment, only the part whose semantics is affected by the change is re-processed. This property is obtained by expressing the language syntax through an operator precedence grammar and by formalizing its semantics through a synthesized attribute schema. We have implemented our technique in a prototype tool and experimentally evaluated its effectiveness. The results show that our approach does not penalize the efficiency of formal verification and can outperform program re-verification after changes, depending on the presence and type of annotations, as well as the position of the change and the program structure.

翻译：增量性是掌握大型、长期运行软件系统复杂性的基本设计原则。该原则已被敏捷开发流程采纳，并构成持续软件演化的基础。在此背景下，一个主要挑战是在每次变更后增量式地重新验证软件工件的正确性，仅将验证工作聚焦于受变更影响的部分。我们提出一种针对KernelC程序（带有用匹配逻辑表达的属性注释）的增量验证方法。该方法基于语法-语义框架，支持代码块隔离分析，从而在程序片段变更后，仅需重新处理语义受该变更影响的部分。此特性通过操作符优先级文法表达语言语法，并利用综合属性模式形式化其语义来实现。我们已在原型工具中实现该技术，并通过实验评估其有效性。结果表明，我们的方法不会损害形式验证的效率，且能根据注释的有无及类型、变更位置及程序结构，在变更后超越程序重新验证的性能。