修改Dafny方法ensure条件后编译成功，是否存在概念误解？

Let's break down what's happening here—your two ensures clauses are actually logically equivalent, so the verification failure isn't due to a core misunderstanding of Dafny concepts. The difference lies in how Dafny's SMT solver processes the structure of your expressions.

First, let's simplify both postconditions to see their equivalence clearly:

Original (failing) ensures clause: #

ensures !((Cache_State[p__Inv2] == S) && (!(Cache_State[p__Inv0] == I)) && (!(Cache_State[p__Inv0] == S)))

Since CACHE_STATE is a datatype with only three possible values (I, S, E), the expression !(Cache_State[p__Inv0] == I) && !(Cache_State[p__Inv0] == S) is exactly equivalent to Cache_State[p__Inv0] == E. Substituting that in, your original clause simplifies to:

ensures !((Cache_State[p__Inv2] == S) && (Cache_State[p__Inv0] == E))

Modified (passing) ensures clause: #

ensures !((Cache_State[p__Inv2] == S) && (Cache_State[p__Inv0] == E ))

This is identical to the simplified version of your original clause!

Why did the original fail to verify? #

The issue comes down to how Dafny's SMT solver handles complex logical expressions and its ability to leverage your preconditions automatically:

1. Your preconditions already guarantee that Cache_State[p__Inv0] != E:
   • You have Chan2_Cmd[i] == GntS and i == p__Inv2, so Chan2_Cmd[p__Inv2] == GntS is true.
   • Combined with the precondition !((Cache_State[p__Inv0] == E) && (Chan2_Cmd[p__Inv2] == GntS)), this simplifies to !(Cache_State[p__Inv0] == E && true) → Cache_State[p__Inv0] != E.
2. After your method runs, Cache_State[p__Inv2] is set to S (since i == p__Inv2 and you execute Cache_State[i] := S;).
3. For the postcondition, the solver needs to prove that !(S && (Cache_State[p__Inv0] == E))—which is trivially true because Cache_State[p__Inv0] != E from your preconditions.

The original clause's nested negations and multiple conjunctions made it harder for the solver to connect the dots between the precondition and the simplified logical state. By rewriting the clause to directly check for Cache_State[p__Inv0] == E instead of the double negation of the other two states, you gave the solver a more direct path to verify the condition.

Key Takeaway #

Dafny's verification relies on the SMT solver's ability to parse and simplify logical expressions. Even when two expressions are logically equivalent, their structure can impact whether the solver can automatically prove them without additional hints. When you run into verification failures with complex boolean logic, try simplifying the expression to its most direct form—this often helps the solver leverage preconditions and method effects more effectively.

内容的提问来源于stack exchange，提问作者Hongjian Jiang