Я новичок в dafny и пытаюсь проверить, является ли каждое целое число четным или нечетным. У меня есть код ниже:
method Main() {
Test();
}
predicate Test (a : int)
{
assert (forall a :: a % 2 == 0 || a % 2 != 0);
}
Но Дафни жалуется, что мой предикат неверен, и я не знаю, почему. Любая помощь приветствуется.
predicate отличается от method тем, что тело predicate должно быть выражением. Например, если вы удалите ключевое слово assert и точку с запятой в конце этой строки, она будет правильно проанализирована.
Кроме того, здесь есть еще несколько проблем. Во-первых, похоже, что Test объявлено принимающим параметр a, но вызов из Main не передает значение для этого параметра. Вы имели в виду, что Test не принимает никаких параметров? Во-вторых, чтобы вызвать predicate из method, вы должны объявить predicate как predicate method, что аналогично predicate, за исключением того, что его можно вызывать из methods.
