viperproject
Feature request: real numbers
For VerCors, I am working on implementing verification of programs that use floating point numbers (for my master thesis). The way that I plan on implementing the support for floating point numbers is by using the real numbers, which are a part of Z3.
A similar tool to Viper, called Why3 (used by other verification tools such as FramaC) has support for real numbers, and Why3 is also based on Z3.
Would it be possible to give access to the real numbers through Viper?
Z3 also supports floating-point numbers directly, which we could lift to Viper. @marcoeilers developed a prototypical extension of Viper for lifting more Z3 types to Viper, but I don't think that feature is merge-ready yet.
A work-around might be permissions, since Viper's Perm types is translated to SMT reals. This work-around would limit you to fractional literals (e.g. 1\3) though, since we don't support floating-point literals (e.g. 0.3).
Could you please indicate how relevant floats are/will be for VerCors? To give us an idea of how urgent your feature request is.
For what it's worth, I updated the floating point support PRs; there were some discussions between Malte and I but I think we agreed that we could merge it in as an experimental feature (it would be experimental anyway, since it only adds support on the AST level, with no syntax and support in the parser yet). So that would be exact IEEE floating point numbers as supported by Z3 (with all the implications, e.g., probably not-too-great performance).
@martijnrenssen PR #428 is the one Marco mentioned. It maybe take a while until it is merged into the Silver code base, but you could locally merge it to see if it suffices for your needs.
Right. That PR only supports IEEE floats though, not reals in the ordinary sense. Those should be easy to support, too, but we'd basically have to build it into Viper directly as a known primitive type I think.
Thanks for the quick responses, IEEE floats are exactly what we want to support in VerCors, so this will be very helpful 👍