如果没有假设合同未经核实，“假设可以证明”不应该出现 [英] 'Assumption can be proven' should not show up if, without the assumption, a contract is not verified

问题描述

添加假设导致'可以证明'警告时非常令人沮丧，但是没有假设会出现不同的警告。

It is very frustrating when adding an assumption causes a 'can be proven' warning, but a a different warning appears without the assumption.

我认为这是由于当假设存在时，有更多可用信息。验证者使用经过验证的假设来证明后置条件，但没有意识到它本身就不会发现这个假设。

I assume this is a consequence of there being more information available when the assumption is present. The verifier uses the proven assumption to prove the postcondition, but doesn't realize that it would not have discovered the assumption on its own.

或者，应该有一种较弱的假设形式，例如作为'提示'。

Alternatively, there should be a weaker form of assumption such as 'Hint'.

推荐答案

嗨Strilanc，

Hi Strilanc,

 我明白。最简单的方法是将这些假设转化为断言。运行时行为是相同的。静态检查器将首先使用断言中的条件来证明以后会出现什么，然后它将证明断言本身。
所以你应该得到没有警告（只有一个更有效的断言）。如果你得到一个，那就是一个bug，我想要一个复制品。

 I understand. The easiest way is to turn those assumptions into assertions. The runtime behavior is the same. The static checker will first use the condition in the assertion to prove whathever comes later, and then it will prove the assertion itself. So you should get no warning (only one more proven assertion). If you get one, then it is a bug, and I'd like to have a repro.

谢谢！

f

 

这篇关于如果没有假设合同未经核实，“假设可以证明”不应该出现的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！