Re: [tlaplus] Real numbers

[Michael Leuschel <leus...@xxxxxxxxxxxxxxxxxxxxx>]

Hi Stephan,

On 12 Oct 2014, at 11:23, Stephan Merz <stepha...@xxxxxxxxx> wrote:

> If there is demand, extending the SMT backend of TLAPS for handling real numbers is not difficult. What fragment of reasoning about real numbers are you interested in? Current solvers behave very erratically outside the fragment of linear real arithmetic, although several groups are looking into different approaches for effectively supporting non-linear real arithmetic: you may want to have a look at dReal (http://dreal.cs.cmu.edu/#!index.md), MetiTarski (http://www.cl.cam.ac.uk/~lp15/papers/Arith/) or Redlog (http://www.redlog.eu).
> 
> The Event-B language as defined by Abrial does not have real numbers (see e.g. http://wiki.event-b.org/images/EventB-Summary.pdf), and as far as I know there is no implementation of its provers that handles real numbers.

That is right.

Jean-Raymond Abrial has, however, developed a first Event-B mathematical extension for reals. I don’t think it is publicly available and there is no automatic proof support, as far as I know.

Real numbers and floats have also been added to the classical-B language within Atelier-B:
 http://www.tools.clearsy.com/tutorials/languages/real-and-floating-point-numbers/

I don’t think there is a lot of proof support though; this was more a proof of concept.

(Our TLA-B and B-TLA translations currently work on classical B but do not support reals, and ProB does not support real or floats (yet) either.)


Greetings,
Michael