[tlaplus] Numerical correctness vs logical correctness

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

I know that TLA+ does not reason about real numbers, but can we model an algorithm which does ?

For example, if the algorithm we want to verify contains a division, and only integer division is supported in TLA+, can we go ahead and model it anyway (if we are interested in other things about it), even though the numerical answer will be wrong? My instinct is that this should not be a problem but I am not 100% sure.

-- 
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/d4b24a56-e945-48b4-af19-b8a16872a87dn%40googlegroups.com.