[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Joana Cruz <jsrcruz@xxxxxxxxx>*Date*: Thu, 22 Apr 2021 08:54:12 -0700 (PDT)

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.

**Follow-Ups**:**Re: [tlaplus] Floating Point operations to check equivalence of algorithms***From:*Isaac DeFrain

**Re: [tlaplus] Floating Point operations to check equivalence of algorithms***From:*Stephan Merz

- Prev by Date:
**[tlaplus] Re: What operators are defined in TLA+ BUILTINS?** - Next by Date:
**Re: [tlaplus] Floating Point operations to check equivalence of algorithms** - Previous by thread:
**[tlaplus] Why was the ? infix operator removed between TLA+ v1 and v2?** - Next by thread:
**Re: [tlaplus] Floating Point operations to check equivalence of algorithms** - Index(es):