Represent an arbitrary 32 bit number in binary form

[Amjad Ali]

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.

[Stephan Merz]

The set of bit vectors of length 32 can be defined as

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

Hope this helps,

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

[Amjad Ali]

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}]?

[Stephan Merz]

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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/34306500-8df5-4703-8c90-019a0acbe150n%40googlegroups.com.

[Amjad Ali]

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.

[Amjad Ali]

Also, is this the correct way to define a couple of variable as 64 bit numbers in binary? :

------------------------------- MODULE model -------------------------------

EXTENDS Integers, Sequences

bv64 == [ {0..63} -> {0,1} ]

xR8  == bv64

xR9  == bv64

xR10 == bv64

xR11 == bv64

xR12 == bv64

xR13 == bv64

xR14 == bv64

xR15 == bv64

=============================================================================

[Andrew Helwer]

The {0 .. 63} should be 0 .. 63. The .. is an ordinary infix operator, it isn't special set syntax so you don't need the surrounding curly braces. {0 .. 63} would just give you a set with a single element, the nested set generated by 0 .. 63.

Andrew