попытка свидетеля null: результат операции может нарушить ограничение типа подмножества

Типы подмножеств и непустота

Определение типа подмножества формы

type MySubset = x: BaseType | RHS(x)

вводит MySubset как тип, обозначающий те значения x типа BaseType, которые удовлетворяют логическому выражению RHS(x). Поскольку каждый тип в Dafny должен быть непустым, существует обязанность доказательства, чтобы показать, что объявленный вами тип имеет некоторый член. Дафни может найти несколько значений-кандидатов и попытается проверить, удовлетворяет ли какое-либо из них RHS. Если кандидаты этого не сделают, вы получите сообщение об ошибке, похожее на то, которое вы видели. Иногда в сообщении об ошибке будет указано, какие значения-кандидаты пробовала Дафни.

В вашем случае единственным значением-кандидатом, которое пробовал Дафни, является значение null. Как указывает Джеймс, значение null даже не достигает первой базы, потому что BaseType в вашем примере является типом ненулевых ссылок. Если вы измените binRelOnS<T> на binRelOnS?<T>, то null имеет шанс быть возможным свидетелем того, что ваш тип подмножества непуст.

Свидетели, предоставленные пользователем

Поскольку Дафни не слишком умен в выборе кандидатов в свидетели, возможно, вам придется предоставить их самостоятельно. Вы делаете это, добавляя предложение witness в конце объявления. Например:

type OddInt = x: int | x % 2 == 1 witness 73

Поскольку 73 удовлетворяет ограничению RHS x % 2 == 1, Дафни принимает этот тип. В некоторых программах может случиться так, что свидетель, который вы имеете в виду, доступен только в фантомном коде. Затем вы можете написать ghost witness вместо witness, что позволит последующему выражению быть призрачным. Свидетель-призрак можно использовать для убеждения верификатора Dafny в том, что тип непустой, но он не помогает компилятору Dafny инициализировать переменные этого типа, поэтому вам все равно придется инициализировать такие переменные самостоятельно.

Используя предложение witness, вы можете попытаться предоставить свой собственный свидетель, используя исходное определение типа подмножества func. Однако предложение свидетеля принимает выражение, а не оператор, что означает, что вы не можете использовать new. Если вы не заботитесь о компиляции своей программы и готовы доверять себе в существовании свидетеля, вы можете объявить функцию без тела, которая обещает вернуть подходящий свидетель:

type MySubset = x: BaseType | RHS(x) ghost witness MySubsetWitness()

function MySubsetWitness(): BaseType
  ensures RHS(MySubsetWitness())

Вам понадобится либо ghost witness, либо function method. Функция MySubsetWitness навсегда останется без тела, так что у вас есть возможность ошибиться относительно некоторого значения, удовлетворяющего RHS.

Предложение witness было введено в Dafny версии 2.0.0. В примечаниях к выпуску 2.0.0 это упоминается, но, по-видимому, не дать много объяснений. Если вы хотите увидеть больше примеров witness, найдите это ключевое слово в наборе тестов Dafny< /а>.

type func<T> = f: binRelOnS?<T> | f.Valid() && f.isFunction()

type func<T> = f: binRelOnS?<T> | f != null ==> f.Valid() && f.isFunction()