Dafny - 在if語句中調用方法？

Question

就像標題所說，我想對修改的另一種方法的if語句裏面的一些變量的方法調用，如：

method A 
... 
{ 
    ... // Modifies some variables 
} 

method B 
... 
{ 
    ... 
    if(statement){ 
     A(); 
    } 
    ... 
} 

這因爲Dafny不起作用不會允許非鬼的方法以這種方式被調用。這個問題的解決方法是什麼？

Answer 1

想通了，可以將其轉換爲一個臨時bool變量，然後使用bool變量中的表達：

... 
var boolean:bool; 
boolean := expression(); 
is(boolean){ 
    ... 
} 
    ...