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

Apr 15, 2013 at 11:06 AM

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

man thanks !

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.

Apr 16, 2013 at 12:00 AM

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 !