[tlaplus] Checking equivalence of two algorithms

["christin...@xxxxxxxxx" <christina.a.burge@xxxxxxxxx>]

Apologies if this is a fairly basic question:

Is it possible to use TLA+ to check if two algorithms always return the same result?

An engineer on my team recently made an optimisation to a routine; interleaving floating point operations with memory operations to make an algorithm run more quickly.

It would seem to me that a good use case would be to check the validity of something like this, but I don't know if that's possible in TLA+. Of course, I can abstract the code sufficiently to the point where the question is essentially "does a+b=b+a?", at which point the proof is perhaps too trivial to be useful.

-- 
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/1d499378-019d-4f83-895a-8fdd09146d94n%40googlegroups.com.