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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Fri, 4 Nov 2022 10:24:26 +0100*References*: <acf45a9b-12cc-4189-8094-750721df34cbn@googlegroups.com> <04554D4D-9760-4011-879E-19745E2AACF4@gmail.com> <34306500-8df5-4703-8c90-019a0acbe150n@googlegroups.com>

Representing a bit vector as a function seems to be natural. If it's more convenient, you can obviously change the index set and number from 0. In TLA+, functions with domain 1 .. N for some natural number N are identified with sequences, which may be convenient for certain purposes. In particular, TLC will print values of the set that I suggested as sequences. But mathematically there is no real difference. For practical purposes, in particular if you aim at verification using TLC, you may find it convenient to make the length of bit vectors a parameter: the set BV32 has 2^32 elements, and TLC won't like enumerating that set. I presume that many algorithms that are correct for bit vectors of length 3 or 4 will also be correct for length 32. 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/90B23BE6-AFD9-4407-A80B-5BC1EB759B96%40gmail.com. |

**Follow-Ups**:

**References**:**[tlaplus] Represent an arbitrary 32 bit number in binary form***From:*Amjad Ali

**Re: [tlaplus] Represent an arbitrary 32 bit number in binary form***From:*Stephan Merz

**Re: [tlaplus] Represent an arbitrary 32 bit number in binary form***From:*Amjad Ali

- Prev by Date:
**Re: [tlaplus] Represent an arbitrary 32 bit number in binary form** - Next by Date:
**Re: [tlaplus] Represent an arbitrary 32 bit number in binary form** - Previous by thread:
**Re: [tlaplus] Represent an arbitrary 32 bit number in binary form** - Next by thread:
**Re: [tlaplus] Represent an arbitrary 32 bit number in binary form** - Index(es):