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

*From*: Ron Pressler <ron.pressler@xxxxxxxxx>*Date*: Thu, 19 Dec 2019 13:03:48 -0800 (PST)*References*: <6215f459-cae9-4f6a-8e65-c15b9f8c4255@googlegroups.com>

Unless what you're specifying is at the level of the hash function itself, you might be thinking about this at too-low a level. If the algorithm you're specifying should work with *any* hash function, make that a part of your specification: ∃ hash ∈ [Source → Bits].... If there are other requirements on the hash, add them to the quantifier. You could also define an override in Java, but then your specification means you rely on that *particular* hash function.

-- Ron

On Thursday, December 19, 2019 at 5:17:37 PM UTC, Thomas Gebert wrote:

On Thursday, December 19, 2019 at 5:17:37 PM UTC, Thomas Gebert wrote:

Hello!I am currently trying to spec out an algorithm that needs a hash algorithm (in this case I have to do things with the bits of the hash, so I can't rely on simple equivalence). It doesn't have to be a cryptographically secure hash, or even a particularly collision-free hash; I just need something that takes in an input, and returns back a consistent number with a consistent input (I'm happy translating the number myself to a binary sequence).Now, I thought about writing a very simple operator to do it with a big if-else chain that simply loops-over a sequence and does a basic number-mapping, then adding the numbers and modding, but then I realized that that would *only* work with Sequences, which means strings wouldn't work.I saw that there was a Stackoverflow post with someone implementing something in Java [0] , and that's what it comes to I'll to that (if someone would link me to how to add custom Java modules into a spec I would be grateful), but I was wondering if I'm overcomplicating this, and maybe there's something built-in now?

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/efea1bc0-807c-438b-9e17-1ee9d4c6c576%40googlegroups.com.

**Follow-Ups**:**[tlaplus] Re: Is there a generic hash function in TLA+?***From:*Thomas Gebert

**References**:**[tlaplus] Is there a generic hash function in TLA+?***From:*Thomas Gebert

- Prev by Date:
**[tlaplus] Re: Is there a generic hash function in TLA+?** - Next by Date:
**[tlaplus] Re: Is there a generic hash function in TLA+?** - Previous by thread:
**[tlaplus] Re: Is there a generic hash function in TLA+?** - Next by thread:
**[tlaplus] Re: Is there a generic hash function in TLA+?** - Index(es):