dafny ошибка нарушения утверждения, не знаю, в чем причина

Я новичок в Дафни. Здесь жалуется, что есть ошибка утверждения:

method Fred () returns (result : int) {
  var number : int;
  result := number * number;
  
  assert result > 0;

}

Я пытаюсь написать утверждение, выражающее следующее утверждение: квадрат любого целого числа неотрицательен.