Re: [tlaplus] Floating Point operations to check equivalence of algorithms

On Thu, Apr 22, 2021 at 9:54 AM Joana Cruz <jsrcruz@xxxxxxxxx> wrote:

Hi,

I have been trying to learn TLA+ and proposed myself as an exercise trying to model the algorithm that is usually used to get the norm of a vector: www.netlib.org/blas/dnrm2.f

However this algorithm makes use of division (SSQ = ONE + SSQ* (SCALE/ABSXI)**2).

I have been having mixed answers on whether division is possible or not. On the one hand in this post Checking equivalence of two algorithms (google.com) sounds like this should be doable.

Older posts (as far as 2014) do say that division on real is not possible, but they also mention the possibility of developing it at some point. Since Z3 is now one of the back end provers for TLA+, I was wondering if it was the case that now real division is supported.

I come to realize that I needed to override the real definition and that enabled the algorithm to be correct when the vector entries are in the set {-1, 0, 1}.

But I wanted to expand this proof upto -5..5 at least.

If it turns out that division is not possible, can anybody point me to any prover/tool where I could model this algorithm?

Thanks,

Joana

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/83feca0e-9080-4c90-b522-5a92f363dec7n%40googlegroups.com.