Можно ли аннотировать параметры метода Дафни как изменяемые, не будучи объектами?
Моя цель - иметь возможность проверить
method testMethod(a:int, b:int) returns (res :int) {
res :=0;
a := (a - b);
assert a < (a-b);
}
Игнорируя тот факт, что это явно абсурдное утверждение, Дафни жалуется на то, что LHS не является изменяемой переменной, а я хотел бы избежать введения временных переменных.
Все внутренние параметры в Dafny являются неизменяемыми (включая внутренние параметры ссылочных типов, хотя с соответствующим предложением modifies метод может вносить изменения в кучу, разыменовывая такой параметр). Итак, вам нужно использовать локальную переменную для хранения выражения a - b в вашем примере. Например:
method testMethod(a:int, b:int) returns (res:int) {
res := 0;
var myLocalA := a - b;
assert myLocalA < myLocalA - b;
}
Если вас беспокоит необходимость вводить новое имя для локальной переменной, Dafny фактически позволяет вам дать локальной переменной то же имя, что и параметру. Если вы считаете, что это в вашем стиле, вы можете написать:
method testMethod(a:int, b:int) returns (res:int) {
res := 0;
var a := a - b;
assert a < a - b;
}
Обратите внимание, что в правой части присваивания локальной переменной a упоминается внутренний параметр a (поскольку локальная переменная a в то время еще не находилась в области видимости).
Если вы делаете это часто, вы также можете начать свой метод с утверждения
var a := a;
Это выглядит нелепо и может сбивать с толку, пока вы не поймете, что происходит, а именно, что этот оператор вводит локальную переменную a и присваивает ее начальное значение значению параметра a.
Причина, по которой входные параметры не могут автоматически использоваться в качестве локальных переменных (что разрешено многими другими языками, включая C и Java), заключается в том, что, по моему опыту, некоторые люди затем путаются в значении входных параметров в постусловиях. . Внутренний параметр, упомянутый в постусловии, относится к значению внутреннего параметра, переданному вызывающей стороной, и это становится ясным, когда внутренние параметры делаются неизменяемыми внутри тела метода.
Рустан
