Boolean logic
Variable
A named place whose value is supplied by an assignment or binder.
Definition
Variable
A variable stands for a value drawn from a declared set or sort.
Boolean variables range over true and false. SMT variables may instead range over integers, real numbers, bit-vectors, strings, or other sorts.
01
Example
In x + 2 = 5, x is a variable whose satisfying integer value is 3.
02
Important distinction
A program variable can change during execution. A logical variable denotes a value within one interpretation unless the formal model represents time explicitly.
After reading this article, you should be able to
- Define Variable in the sense used on this site.
- Identify a variable's allowed values from its declared sort.