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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sat, 24 Apr 2021 08:36:17 +0200*Ironport-hdrordr*: A9a23:VgqVcK+COlT6d6j46+tuk+EVdr1zdoIgy1knxilNYDRvWIixi92ukPMH1RX9lTYWXzUalcqdPbSbKEmxhOVIyKErF/OHUBP9sGWlaLtj44zr3iH6F0TFm58k6Y5JSII7MtH5CDFB57eC3CCTFdE8zN6btJ25nOu29QYccShGSYFFqz14BAGSD1FsSGB9avQEPbeV+8YvnUvURV05dcK+b0N1LtTrh9qOr57+ZA5DOhhP0nj5sRqM6KTmVzCC1BYfTD8n+8ZmzUHhkxblooSutujT8G6f60b3745K3PvNo+EzSvCkr8gON3HUjBy0Db4RGIGqmTAuvaWS70w3m8PHuBcqM61ImjfsV0W8oR7s3Ael1TY19hbZuBClqF/uu9bwSj5/K8cpv/MRTjL8604t+O5xy7hK2WXxjeslMTr4hyj269XFUBtn/3DE7UYKquIYg3xBXYZ2UtY4xv15jTklbOZ/IAvA5IoqEPZjAYXn3dk+SyLmU1njsmZi29CqVHgody32NnQqgcCN1igToXYR9TpU+OUkknAM+IlVcfl5zt7ZOadlnqwmdL5lUYtBAo46MLyKI12Iah7BN1+SLU/qfZt3X07lmtrY5PEQ6PuxcJIFiKEukInMOWko1lIaSgbBD8uB2ZEO3zLsZCGGXTrrwtxD/JQRgNzBbYuuHyuERlUj1+W6pekHRu3XMszDeK5+MrvMK23hHIoM5QniQt1pL2UEWsF9gKdYZ3u+5ubCKojnrYXgAb7uDYuoNy0lVGP5Cn5GdCTvJclG80CgUmL5hh+UYH/2Zknj5/tLYeLn1tlW7pMMOI1Kug1Qs1i/682RQAcy+ZAeTQ9ELLnqkry2qACNjAO4iRQXBjNtSnxN6LGleXJHrw0HPgfVdvIsoNOCYAlprTq6GiM=*References*: <d4b24a56-e945-48b4-af19-b8a16872a87dn@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
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/862EFD8E-1E6D-43B4-92CD-A707E1081FB1%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Numerical correctness vs logical correctness***From:*c.burge...@xxxxxxxxx

**References**:**[tlaplus] Numerical correctness vs logical correctness***From:*christin...@xxxxxxxxx

- Prev by Date:
**[tlaplus] Re: Numerical correctness vs logical correctness** - Next by Date:
**Re: [tlaplus] TLAPS proof of increment and update** - Previous by thread:
**[tlaplus] Re: Numerical correctness vs logical correctness** - Next by thread:
**Re: [tlaplus] Numerical correctness vs logical correctness** - Index(es):