CODEWITHSUNDEEP
dafny
henry_1920
henry_1920

Reputation: 1

dafny assertion violation error, not sure what the reason is

I am very new to Dafny. It is complaining here that there is an assertion error:

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

}

I am trying to write an assertion that expresses the following statement: the square of any integer is non-negative

Upvotes: 0

Views: 72

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

The assertion passes if you change it to result >= 0. Is that what you meant? If number is 0, then result will be 0 too.

Upvotes: 1

Related Questions