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

Re: [tlaplus] Represent an arbitrary 32 bit number in binary form

You made a great point about there being 2^32 elements. I do in fact have to verify and prove some things regarding this in the future. My idea was to prove by induction.

On Friday, November 4, 2022 at 4:24:32 AM UTC-5 Stephan Merz wrote:
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

On 4 Nov 2022, at 10:15, Amjad Ali <amjad.h...@xxxxxxxxx> wrote:


Thank you for the answer! So, would this be considered a set of functions? Also, would I be able to modify the answer as BV32 == [0..32 -> {0,1}]?
On Thursday, November 3, 2022 at 4:06:14 AM UTC-5 Stephan Merz wrote:
The set of bit vectors of length 32 can be defined as

BV32 == [ 1 .. 32 -> {0,1} ]

Hope this helps,
Stephan


On 3 Nov 2022, at 09:46, Amjad Ali <amjad.h...@xxxxxxxxx> wrote:

What is the most mathematical way of defining a binary number in TLA+.
My guess is something like the following:

data32 == << b_0 \in {0,1}, ... ,  b_31 \in {0,1} >>

However, this results in a syntax error.




--
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...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/acf45a9b-12cc-4189-8094-750721df34cbn%40googlegroups.com.


--
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...@xxxxxxxxxxxxxxxx.

--
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/f1b09c3e-ab57-4466-9eb6-0f4ece826365n%40googlegroups.com.