[Vaton] How to add support for string to fixed-point with SPARK proof?

General
1

As @mhatzl suggests, I open this topic to discuss about: [REQ] Support for fixed-point numbers · Issue #3 · mhatzl/vaton · GitHub

For those not familiar, Vaton is a “verified ASCII to number conversion written in Ada/SPARK.”

This lib currently supports the following types:

  • Integer representing Standard.Integer
  • Long_Integer representing Standard.Long_Integer
  • Long_Long_Integer representing Standard.Long_Long_Integer
  • Big_Integer representing Ada.Numerics.Big_Numbers.Big_Integers.Valid_Big_Integer
  • Float representing Standard.Float
  • Long_Float representing Standard.Long_Float
  • Long_Long_Float representing Standard.Long_Long_Float
  • Big_Real representing Ada.umerics.Big_Numbers.Big_Reals.Valid_Big_Real

I would like to also be able to support fixed-point, but we do not find a way to have a proven fixed-point conversion.

As someone have ideas how to do it?

5 Likes