The use of function contracts to specify the behavior of functions often remains limited to the scope of a single function call. Relational properties link several function calls together within a single specification. They can express more advanced properties of a given function, such as non-interference, continuity, or monotonicity. They can also relate calls to different functions, for instance, to show that an optimized implementation is equivalent to its original counterpart. However, relational properties cannot be expressed and verified directly in the traditional setting of modular deductive verification. Self-composition has been proposed to overcome this limitation, but it requires complex transformations and additional separation hypotheses for real-life languages with pointers. We propose a novel approach that is not based on code transformation and avoids those drawbacks. It directly applies a verification condition generator to produce logical formulas that must be verified to ensure a given relational property. The approach has been fully formalized and proved sound in the Coq proof assistant.
翻译:功能合同用于指定函数的行为通常仍限于单一函数调用的范围。 关系属性将多个函数在单一规格内连接在一起。 它们可以表达特定函数的更高级属性, 如不干预、连续性或单调性。 它们还可以与不同的功能相联系, 例如, 以显示优化实施与其原始对应功能相当。 但是, 在传统的模块式扣减核查环境中, 无法直接表达和核实关联属性。 已经提议了自我组合以克服这一限制, 但需要复杂的转换和额外的分解假设, 并且需要用指针对实时语言进行分解。 我们提议一种新颖的方法, 不以代码转换为基础, 避免这些偏差。 它直接应用核查条件生成了逻辑公式, 以确保给定的关联属性。 这种方法在Coq验证助理中已经完全正规化, 并被证明是可靠的。