Почему проверка этого примера с Dafny не удалась?
Ответ Денниса правильный. Однако я хотел бы объяснить это решение немного более подробно (для пользователя Windows):
- Зайдите в свое меню «Пуск» и введите
regeditв поле поиска. - Перейдите к пути
HKEY_LOCAL_MACHINE\Software\JavaSoft(теперь у Windows 10 есть это:HKEY_LOCAL_MACHINE\Software\WOW6432Node\JavaSoft) - Щелкните правой кнопкой мыши папку JavaSoft и нажмите
New->Key - Назовите новый ключ
Prefs, и все должно работать.
В качестве альтернативы сохраните и выполните файл *.reg со следующим содержимым:
Windows Registry Editor Version 5.00
[HKEY_LOCAL_MACHINE\Software\JavaSoft\Prefs]
1 ответ
Да, вы можете получить контрпример. Если вы используете Visual Studio, просто нажмите на красный круг, где ошибка. Это вызывает отладчик проверки. Если вы используете VS Code, нажмите F7 (см. https://marketplace.visualstudio.com/items?itemName=correctnessLab.dafny-vscode ). Это подтвердит вашу программу и покажет вам некоторую информацию из контрпример.
В вашем случае эти контрпримеры показывают x и y как равные и изначально x[0]==y[0]==1. Действительно, начиная с этого начального состояния, test5 не будет устанавливать заявленное постусловие.
Rustan