Dafny - Методы вызова внутри операторов if?

Как следует из названия, я хотел бы вызвать метод, который изменяет некоторые переменные внутри оператора if другого метода, например:

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

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

Это не работает, так как Dafny не позволяет вызывать методы, не являющиеся призраками, таким образом. Каким может быть обходной путь к этой проблеме?

if-statement dafny

David S 01.12.2015 источник

arrow_upward
1
arrow_downward

Разобрался, могу привести его к временной логической переменной, а затем использовать логическую переменную в выражении:

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

David S 01.12.2015