Изменение параметров метода - PullRequest
Новая
       5

Изменение параметров метода

0 голосов
/ 04 июля 2018

Можно ли аннотировать параметры метода Дафни как изменяемые, не будучи объектами?

Моя цель - иметь возможность проверить 

method testMethod(a:int, b:int) returns (res :int) {
  res :=0;
  a := (a - b);
  assert a < (a-b);
}

Игнорируя тот факт, что это, очевидно, абсурдное утверждение, Дафни жалуется на то, что LHS не является изменяемой переменной, хотя я бы хотел избежать введения временных переменных.

1 Ответ

0 голосов
/ 05 июля 2018

Все входные параметры в 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), заключается в том, что, по моему опыту, некоторые люди запутываются в значении параметры в постусловиях. Указанный в постусловии параметр in относится к значению входного параметра, передаваемого вызывающей стороной, и это становится понятным, если сделать параметры неизменными внутри тела метода.

Rustan

...