[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Checking equivalence of two algorithms
- From: "christin...@xxxxxxxxx" <christina.a.burge@xxxxxxxxx>
- Date: Fri, 26 Mar 2021 06:51:46 -0700 (PDT)
- Ironport-hdrordr: A9a23:Ecd86qmFKheco1FR7wkGHw6tW2npDfPiimdD5ilNYBxZY6WkvuillvgDyFvQgDEeRHkvlbm7Sc29aFnb8oN45pRUGL+kUhXvtmfAFvAE0aLJxTr8FyristNMzKsISdkDNPTcBUV35Pyb3CCWCNAlqePrzImJgqPkw25pXUVWbchbnmJEIyK6NmEzewVcH5o+E/Onl7V6jh6tY24eYMj+JlRtZZmhm/TxmJjrYQELCnccgWHk5w+A07L0HwOV2R0TSVp0sNUf2FLYmA/07LjLiZ6G4yLczGPa4tB3n9bs27J4ZfCkt8kPJj3gzjuvfYRqMoftgBkJpoiUhGoCoZ3pmVMAN942w27Ndmu1yCGdvTXI4XIL0Tve7nO2xVHkutf0QTomDdEpv/MhTjLE8UY6+Nlz3KVXtljpz6Z/HFfFhmDw9tLIXxZlmg6xrWA5meAelXBZTJATcaRct4AZ4UNTHooRBS6S0vFdLMB+SMXHoPpGe1KTaH7U+nR1yNu3R3IpA1OIWU4HtsuJ0yVHnXxwwkcCrfZv5Eso5dY6UJlL5+PNL6RumvVPV6YtHN9AONs=
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.