Это информационное сообщение (не ошибка), и оно довольно неясное! (Мне пришлось самому разобраться в этом, чтобы понять это.)
Когда есть обязательство по доказательству, включающее предикат (здесь LessThanOrEqual), тогда верификатор Dafny внутренне настраивает все так, что если он не сможет Докажи предикат, он сможет сказать тебе, какой конъюнкт внутри тела предиката терпит неудачу. Вы увидите это как сообщения «связанного объявления», которые сопровождают сообщения об ошибках.
Вы можете думать о том, что происходит, по сути, встраивая тело предиката в сайт вызова предиката. Иногда, однако, это не может быть сделано. Например, если предикат является рекурсивным, тогда должно быть некоторое ограничение для такого встраивания. Если встраивание не может быть выполнено, это означает, что любое сообщение об ошибке, которое вы получите, просто скажет «не может доказать LessThanOrEqual(...)», но не сообщит вам, с какой частью определения LessThanOrEqual не удалось справиться. доказать.
Более тонкая причина того, почему нельзя сделать встраивание, связана с квантификаторами. Верификатор работает с квантификаторами через так называемые совпадающие триггеры . Триггер информирует верификатор, когда было бы неплохо создать экземпляр квантификатора. Существуют определенные правила о том, что может и не может быть триггером. Единственное правило, которое относится к вашему примеру, состоит в том, что арифметика c + не может быть частью триггера. Я предполагаю, что определение вашего LessThanOrEqual включает квантификатор, и что верификатор выбирает в качестве триггера этого квантификатора термин, который включает второй параметр LessThanOrEqual. Если бы вышеприведенный вызов LessThanOrEqual был встроенным, то + пробрался бы в триггер, и это не разрешено правилом.
Таким образом, Дафни решил не включать этот вызов в LessThanOrEqual. Все это означает, что вы бы получили чуть менее точное местоположение ошибки, если бы верификатор не смог доказать утверждение. Вы, вероятно, не заметили бы или не беспокоились об этом; действительно, получение менее точного сообщения об ошибке, вероятно, менее озадачивает, чем информационное сообщение, которое вы получаете вместо этого.
Существует способ подавления информационного сообщения: если вы передаете эквивалентное выражение, которое прямо не упоминает +. Например, вы можете использовать локальную переменную:
ghost var s := a[z+1..r];
assert LessThanOrEqual( [a[z]], s );
или выражение let:
assert var s := a[z+1..r]; LessThanOrEqual( [a[z]], s );
Rustan