Как упоминалось в вики на Dafny GitHub, когда Dafny не может доказать утверждение в программе, это может быть связано либо с неверной моей программой, либо с незавершенностью Dafny. Но я подумал, что контрпример от Дафни поддельный после того, как я попытался понять его, поэтому я до сих пор не знаю, правильна ли моя программа.
Мой вопрос заключается в следующем.
Если мне удастся использовать другой сервер Boogie, такой как Corral, для проверки переведенной программы Boogie от Dafny, используя /print, и Corral также вернет модель для аннулирования программы Boogie, это будет гарантировать, что модель опровергнет мою программу Dafny, и я смогу использовать ее для отладки? Или это все еще может быть ложным, так что не пытайтесь попробовать?
Из их статей мне кажется, что Corral и Symbooglix должны гарантировать, что предоставленная модель будет конкретным контрпримером для переведенной программы Boogie, поэтому, возможно, мой вопрос больше о том, является ли программа Dafny и переведенная программа Boogie семантически эквивалентный.
PS: я попытался передать переведенные bpl-файлы в Corral и проверить конкретную процедуру Boogie в этом bpl, и Corral просто говорит, что не может найти процедуру, поэтому я спорю, хочу ли я заставить ее работать.