Numerical correctness vs logical correctness

33 views
Skip to first unread message

christin...@gmail.com

unread,
Apr 23, 2021, 4:49:12 PM4/23/21
to tlaplus
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.

Andrew Helwer

unread,
Apr 23, 2021, 9:26:42 PM4/23/21
to tlaplus
One way to do this is to implement a Rationals module, and define your algorithm to work over the Rationals instead of the Reals. This would be amenable to finite model checking. Or, if your problem is amenable to it, define your algorithm inputs such that integer division will always give the same answer as division over the Reals.

Using floating point with model checking is difficult because you can't easily check equality between two states due to accumulation of errors.

Andrew

Stephan Merz

unread,
Apr 24, 2021, 2:36:22 AM4/24/21
to tla...@googlegroups.com
If your algorithm does not at all depend on the result of division, you can replace it by a constant parameter Div(_,_). For theorem proving, you should then be able to prove the properties that you are interested in. For model checking, you will still need to provide an instance of that operator, say

Div(x,y) == 42

but you can run TLC with different definitions to become confident that the definition is indeed irrelevant. However, if this is true, it sounds like you could write an even more abstract specification, such as getting rid of variables to which division is applied.

If your algorithm depends on certain properties of division but not the precise result you can state those in an ASSUME clause, say,

ASSUME \A x,y \in Int : y # 0 => Div(x,y) \in Int /\ Div(x,y) < x

Stephan

On 23 Apr 2021, at 22:49, christin...@gmail.com <christin...@gmail.com> wrote:

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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d4b24a56-e945-48b4-af19-b8a16872a87dn%40googlegroups.com.

c.burge...@gmail.com

unread,
Apr 26, 2021, 6:57:43 AM4/26/21
to tlaplus

Thank you! A number of different approaches to consider then! 
Reply all
Reply to author
Forward
0 new messages