нарушение ассертов в МВС с Дафни, но проверено в Rise4fun

https://rise4fun.com/Dafny/ZkKN

Это утверждение не проверяется Dafny 2.3.0. над MVS, но проверено вrise4fun, естественно с предупреждением о триггерах. Это вызывает «Проверка неубедительна».

Более того, https://rise4fun.com/Dafny/Um6t не печатает "привет" (не бег) в Rise4fun. Это должна быть какая-то ошибка, так как нет «нарушения утверждения». Пожалуйста, помогите?


dafny
person jiplucap    schedule 09.10.2019    source источник
comment
Время ожидания обоих файлов истекло. Как вы определили, что первое проверено в Rise4fun? Тайм-аут также является причиной того, что приветствие не печатается.   -  person Matthias Schlaipfer    schedule 11.10.2019

Ответы (1)


arrow_upward
0
arrow_downward

Ваша программа проверяет, когда я добавляю флаг -arith:2, который добавляет символические синонимы для арифметических символов и позволяет использовать их в триггерах.

Изменить: более общий ответ заключается в том, что в вашей задаче используется нелинейная арифметика, которая в общем случае неразрешима. Несколько советов о том, как с ними справиться, можно найти в FAQ по адресу https://github.com/dafny-lang/dafny/wiki/FAQ, однако у меня нет большого опыта работы с Dafny и нелинейной арифметикой.

Я не знаю, почему ваш файл работал раньше, но для исследования вы можете распечатать кодировку SMT, которую Dafny подает на Z3 (см. smt-file/57237474#57237474">dafny выводить как файл SMT) и сравнивать разные версии, если нет разницы, может есть разница между версиями Z3.

Может быть, есть способ кодировать вашу проблему по-другому, который работает более стабильно между разными версиями решателя, при условии, что ни в одном из инструментов нет ошибок.

person Matthias Schlaipfer    schedule 14.10.2019
comment
Извините, я написал новый комментарий до прочтения этого. Спасибо за эту помощь. - person jiplucap; 14.10.2019
comment
Спасибо Матиасу за эту помощь. Действительно, флаг работает во всех моих примерах. Но я должен сказать, что предыдущие версии Dafny не нуждались в каких-либо флагах для проверки такого рода утверждений. - person jiplucap; 14.10.2019
comment
Извините, но в rise4fun.com/Dafny/Um6t флаг НЕ РЕШАЕТ ПРОБЛЕМУ - person jiplucap; 14.10.2019
comment
Еще раз спасибо за вашу помощь и предложения. Извините за настойчивость, но, пожалуйста, взгляните на это: rise4fun.com/Dafny/v6pN. Флаг не работает. - person jiplucap; 14.10.2019
comment
Является ли method {arith:2} ... действительным Дафни? Это работает, когда вы звоните dafny -arith:2 <yourfile> - person Matthias Schlaipfer; 14.10.2019
comment
Синтаксически правильно, парсер не жалуется. - person jiplucap; 15.10.2019
comment
Здесь rise4fun.com/Dafny/hzt9 вы можете найти решение, которое предложил мне Рустан Лейно (год назад ), но я бы хотел, чтобы в самой последней версии Dafny было что-то более простое для моих учеников. Какой-то флаг, работающий в MVS или около того. - person jiplucap; 15.10.2019
comment
Добавление такой непрозрачной функции должно быть эквивалентно использованию флага -arith. Вы можете попробовать ввести такие функции для всех арифметических операторов. - person Matthias Schlaipfer; 15.10.2019
comment
Кроме того, я подозреваю ошибку, потому что в следующем rise4fun.com/Dafny/Y03M первое утверждение верно, но прокомментированное нарушено. Пожалуйста, раскомментируйте его и проверьте. - person jiplucap; 15.10.2019
comment
В вашем последнем примере утверждения отличаются. Рассмотрим t = 2, e = 1. Можете ли вы объяснить, почему, по вашему мнению, утверждение должно выполняться? Сейчас у меня нет времени углубляться в это. - person Matthias Schlaipfer; 15.10.2019
comment
Да, они разные, но одно является следствием другого. Действительно, второй сильнее, я ошибочно думаю, что сильнейшим был первый. Для его реализации следует учесть, что (a ==› ((b && c) || ​​(!b && d)) ==› (a ==›( (b && c) || ​​(d))), а второй имеет вид (a ==› ((b && c) || ​​(!b && d)) ), а первый — (a ==› ((b && c) || ​​(! б && г) )), кроме универсального замыкания. - person jiplucap; 15.10.2019
comment
Давайте продолжим обсуждение в чате. - person jiplucap; 15.10.2019
comment
Возвращаясь к моей исходной задаче, не связанной со вспомогательной леммой, я нахожу нечто, в чем не могу разобраться. Утверждения на сайте ride4fun.com/Dafny/9fAslB наводят меня на мысль, что что-то идет не так. Верификатор имеет странное поведение. Пожалуйста, раскомментируйте только один в каждом тесте. Есть что-то, связанное с физ, но я думаю, что это не связано с индукцией. - person jiplucap; 17.10.2019
comment
У меня немного другое поведение, чем у вас, но когда я добавляю -arith:2, все они проверяются. - person Matthias Schlaipfer; 17.10.2019
comment
В моем случае, используя {:arith 2} после ключевого слова assert или после ключевого слова method (оба допустимы в Dafny 2.3.0), все, кроме одного, проверяются, но самая интригующая проблема заключается в том, что этот самый простой: assert {:arith 2} forall b,e,x,t,p :: (0 ‹= t ‹= e && p * power(x,t) == power(b,e) && t › 0 ) == › (0 ‹= t-1 ‹= e && p * x * power(x,t-1) == power(b,e)); Это также не работает в Rise4fun. - person jiplucap; 17.10.2019
comment
Я думаю, что {:arith 2} не влияет. По крайней мере, в моей версии Dafny этого нет. Вы можете проверить это, сгенерировав файл smt2, используя -proverLog:<smt2file> с {:arith 2}, добавленным к утверждению и без него, и запустив diff для файлов. - person Matthias Schlaipfer; 17.10.2019
comment
Да, но я не знаю, почему это происходит в данном случае, ведь некоторые непроверенные утверждения в моих предыдущих примерах были проверены, когда я добавил флаг {:arith 2}. Еще раз спасибо. - person jiplucap; 22.10.2019