Booleans

Booleans are the foundation of all logical reasoning. Because Quint is built fundamentally upon the Temporal Logic of Actions (TLA), describing how a system changes over time relies heavily on the basic concepts of boolean logic. Furthermore, since guards, properties and quantifiers all ultimately produce or consume bool values, the concepts and operators that we cover here will appear very often on your specifications. In this lesson, you will learn how to work with booleans in Quint and how to take full advantage of what the language’s syntax has to offer.

What this lesson covers:

• Boolean literals (true and false).
• Built-in logical operators.
• N-ary alternatives for and and or operators.
• Alternative calling forms (dot notation and block form).

Boolean Literals

Quint has two built-in values of bool type, called boolean literals:

• false is the value that represents the value “false”.
• true is the value that represents the value “true”.

  // false is a built-in constant
  pure val myFalse = false
 
  // true is a built-in constant too
  pure val myTrue = true

Note that Quint is strict with respect to boolean values. There are only false and true. They cannot be compared to values of other types, and there are no implicit conversions from other types to the boolean type.

Boolean values are immutable. The values themselves cannot be modified, but they can be carried around as variable values, or in data structures.

Built-in Operators

Quint provides standard logical operators. If you have a background in formal logic, they will look very familiar to you. The table below summarizes them in order from highest to lowest precedence.

You can try several possible combinations of false and true with these operators in the REPL to check your intuition about them. While negation, conjunction and disjunction operators are very common and broadly understood, there are some interesting things to say about equality and implication.

Equality

Notice that the equality (==) and inequality (!=) operators are generic. Their signature (t, t) => bool means they can compare any two values, provided they are of the exact same type t. Because Quint is strictly typed, this guarantees that a boolean can only ever be compared to another boolean. Try these in the REPL:

  0 == 0          // evaluates to true

  true == true    // evaluates to true

  0 == true       // triggers an error

For a boolean-specific equivalence operator, you can use iff. The statement a iff b is stricter than a == b, as its signature requires both a and b to be booleans. Let’s try it in our REPL session:

true iff true     // evaluates to true

0 iff 0           // triggers an error

This operator shines when working with mathematical properties. Consider verifying that the factored and expanded forms of the difference of squares always agree. We would expect the following definitions to always evaluate to true, independently of the value of their arguments:

pure def differenceOfSquaresEq(a, b, c)  = (a^2 - b^2 == c)  == ((a + b) * (a - b) == c)

pure def differenceOfSquaresIff(a, b, c) = (a^2 - b^2 == c) iff ((a + b) * (a - b) == c)

Both definitions are technically equivalent, but the second reads naturally as the factored form equals c if and only if the expanded form equals c, while the first one buries the logical relationship inside a value comparison, and the nested == makes it easy to mistake a logical claim for an arithmetic one.

We will see iff used this way extensively in invariants and temporal formulas, covered in follow-up lessons.

Logical Implication

Boolean implication, written as a implies b in Quint (or a -> b / a => b in some other languages) is equivalent to saying: “if a is true then b must also be true”.

You can try these on the REPL to see how the truth table of this operator looks like:

true.implies(true)

true.implies(false)

false.implies(true)

false.implies(false)

In fact, a implies b is syntactic sugar for not(a) or b. While it does not add new logical expressiveness to the language, it is incredibly useful for clearly stating that one condition naturally follows from another.

Consider this example: if we want to assert that a message must have been sent in order to be delivered, we could write something like: delivered(m) implies sent(m).

This makes our intention very clear: if a message is delivered, then it must have been sent. However, we could have achieved the exact same logic by writing: not(delivered(m)) or sent(m), but the underlying intent becomes much harder to grasp at a glance.

There is a third equivalent way to express this. Although we will dive deeper into flow operators in a follow-up lesson, you can also write an implication using an if/else statement, which is very natural for most programmers:

if (a) b else true

Because all three of these statements will always evaluate to the exact same result, choosing between them ultimately comes down to context and your own personal taste. That said, implies often expresses intent most directly, making your specifications much easier to read.

N-ary operators

Sometimes we need to work with predicates that operate over many terms, writing deeply nested expressions like:

and(true, and(false, and(true, and(and(false, false), true))))

Such an expression can be very visually noisy, making it easy to misread or to accidentally introduce a mistake. Fortunately, Quint’s and and or operators are not restricted to just two arguments. Because they are n-ary operators, they can accept any (positive) number of arguments. By taking advantage of this and the associative property of conjunction, we can write the previous expression in a much simpler way:

and(true, false, true, false, false, true)

Try evaluating these expressions in the REPL yourself:

and(true, false, true)

or(true, false, true, false)

and(true, false, true, false, true)

The following sections will introduce alternative ways to structure the logic in your specifications, further helping you expand your toolkit with strategies to keep complex expressions readable.

Alternative Calling Forms

Even with n-ary operators, as your boolean expressions grow, they can easily produce long chains of arguments that are hard to follow. Because you will frequently write extensive boolean statements throughout your specifications, Quint provides several alternative calling forms designed specifically to keep your specs clean, readable, and easy to reason about.

Dot Form

All of Quint’s operators support an object-oriented calling style, commonly referred to as dot notation. Try this in the REPL:

  // this is equivalent to and(false, true, false)
  false.and(true, false) 

This form is especially useful for flattening nested formulas into readable chains:

  // equivalent to and(and(x, y), z)
  x.and(y).and(z)

This is a general principle: You can always replace bar(x, y) with x.bar(y), and vice versa. This applies universally to all other Quint operators (not only booleans), including the custom ones you write yourself. However, when calling unary operators, remember to always include the empty parentheses. While false.not() is perfectly valid, false.not will trigger an error, as Quint will try to interpret it as a record field access.

Block Form

When and and or expressions get bigger, you can wrap them in {...}, stack them in blocks and format them vertically. This allows you to write:

and {
  p_1,
  p_2,
  ...
  p_n,
}

or {
  p_1,
  p_2,
  ...
  p_n,
}

The trailing comma after the final item p_n is optional, and n must be a positive number. These are just syntactic sugar for the standard and(p_1, p_2,..., p_n) and or(p_1, p_2,..., p_n) calling forms respectively, but they can be incredibly useful for improving readability. Try the following example on your REPL session to see how it works:

and {false == false, true == true}

Summing it up

In this lesson, we covered the essentials of working with booleans in Quint. Quint has exactly two values of type bool: true and false. They are immutable, strictly typed, and never implicitly converted from other types. A boolean can only ever be compared to another boolean.

We explored the standard logical operators not, and, or, iff, and implies, along with the generic == and !=. Each operator has both an infix and a named calling form (except for not that only has a named one), and they are evaluated in a fixed precedence order. We discussed the distinction between == and iff, along with the equivalent logical expressions for implication.

Finally, we looked at how to keep your specifications clean as your logic naturally grows in complexity. By leveraging and and or as n-ary operators, using the object-oriented dot form for reading chains left-to-right, and vertically stacking long expressions using the block form, you can ensure your complex boolean statements remain readable, maintainable, and easy to reason about.