Using different data types in Dafny "except int and nat"

Apr 15, 2013 at 11:06 AM
HI,

anyone can tell that how we can use or define the data types in Dafny such as strings , dates, floats etc.

man thanks !

-asif
Coordinator
Apr 15, 2013 at 8:53 PM
Dafny does not have any pre-defined string or float types. If you don't need a lot of operations on them, then you can use sequences (of what would be characters) for strings. You can also simulate floats by a pair of integers, one to represent the mantissa and one to represent the exponent. Some day, I'd like to see strings or reals in Dafny (are you interested and in a position to add them to the Dafny implementation?).

For more information on how to define datatypes (including records and enumerations), see the Dafny quick reference.

Rustan
Apr 16, 2013 at 12:00 AM
Hi,

many thanks for clarifications. I am working on a project for Dafny, as soon as i completed this one, i may be able to work on that.

thanks !
-asif