CODEWITHSUNDEEP
dafny
Kevin S
Kevin S

Reputation: 531

What are real numbers in Dafny?

What are real numbers in Dafny. Are they represented as IEEE 754-2008 floating point numbers? If not, then what are they? I.e., what is the specification of the real type in Dafny?

Upvotes: 3

Views: 665

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

Dafny's real numbers are not floating point numbers.

From a verification perspective, they are the mathematical real numbers, and Dafny reasons about them using Z3's theory of real arithmetic.

From a compilation perspective, Dafny actually compiles them to BigRationals, which is made possible by the fact that Dafny doesn't have any builtin operations for creating irrational real numbers.

Upvotes: 4

Related Questions