Lesson 1.6: Integers and Booleans
The purpose of this lesson is to explain the two most basic types of builtin
sorts in K, the Int
sort and the Bool
sort, representing
arbitraryprecision integers and Boolean algebra.
Builtin sorts in K
K provides definitions of some useful sorts in
domains.md, found in the
include/kframework/builtin
directory of the K installation. This file is
defined via a
Literate programming
style that we will discuss in a future lesson. We will not cover all of the
sorts found there immediately, however, this lesson discusses some of the
details surrounding integers and Booleans, as well as providing information
about how to look up more detailed knowledge about builtin functions in K's
documentation.
Booleans in K
The most basic builtin sort K provides is the Bool
sort, representing
Boolean values (i.e., true
and false
). You have already seen how we were
able to create this type ourselves using K's parsing and disambiguation
features. However, in the vast majority of cases, we prefer instead to import
the version of Boolean algebra defined by K itself. Most simply, you can do
this by importing the module BOOL
in your definition. For example
(lesson06a.k
):
kmodule LESSON06A imports BOOL syntax Fruit ::= Blueberry()  Banana() syntax Bool ::= isBlue(Fruit) [function] rule isBlue(Blueberry()) => true rule isBlue(Banana()) => false endmodule
Here we have defined a simple predicate, i.e., a function returning a
Boolean value. We are now able to perform the usual Boolean operations of
and, or, and not over these values. For example (lesson06b.k
):"
kmodule LESSON06B imports BOOL syntax Fruit ::= Blueberry()  Banana() syntax Bool ::= isBlue(Fruit) [function] rule isBlue(Blueberry()) => true rule isBlue(Banana()) => false syntax Bool ::= isYellow(Fruit) [function]  isBlueOrYellow(Fruit) [function] rule isYellow(Banana()) => true rule isYellow(Blueberry()) => false rule isBlueOrYellow(F) => isBlue(F) orBool isYellow(F) endmodule
In the above example, Boolean inclusive or is performed via the orBool
function, which is defined in the BOOL
module. As a matter of convention,
many functions over builtin sorts in K are suffixed with the name of the
primary sort over which those functions are defined. This happens so that the
syntax of K does not (generally) conflict with the syntax of any other
programming language, which would make it harder to define that programming
language in K.
Exercise
Write a function isBlueAndNotYellow
which computes the appropriate Boolean
expression. If you are unsure what the appropriate syntax is to use, you
can refer to the BOOL
module in
domains.md. Add a term of
sort Fruit
for which isBlue
and isYellow
both return true, and test that
the isBlueAndNotYellow
function behaves as expected on all three Fruit
s.
Syntax Modules
For most sorts in domains.md
, K defines more than one module that can be
imported by users. For example, for the Bool
sort, K defines the BOOL
module that has previously already been discussed, but also provides the
BOOLSYNTAX
module. This module, unlike the BOOL
module, only declares the
values true
and false
, but not any of the functions that operate over the
Bool
sort. The rationale is that you may want to import this module into the
main syntax module of your definition in some cases, whereas you generally do
not want to do this with the version of the module that includes all the
functions over the Bool
sort. For example, if you were defining the semantics
of C++, you might import BOOLSYNTAX
into the syntax module of your
definition, because true
and false
are part of the grammar of C++, but
you would only import the BOOL
module into the main semantics module, because
C++ defines its own syntax for and, or, and not that is different from the
syntax defined in the BOOL
module.
Here, for example, is how we might redefine our Boolean expression calculator
to use the Bool
sort while maintaining an idiomatic structure of modules
and imports, for the first time including the rules to calculate the values of
expressions themselves (lesson06c.k
):
kmodule LESSON06CSYNTAX imports BOOLSYNTAX syntax Bool ::= "(" Bool ")" [bracket] > "!" Bool [function] > left: Bool "&&" Bool [function]  Bool "^" Bool [function]  Bool "" Bool [function] endmodule module LESSON06C imports LESSON06CSYNTAX imports BOOL rule ! B => notBool B rule A && B => A andBool B rule A ^ B => A xorBool B rule A  B => A orBool B endmodule
Note the encapsulation of syntax: the LESSON06CSYNTAX
module contains
exactly the syntax of our Boolean expressions, and no more, whereas any other
syntax needed to implement those functions is in the LESSON06C
module
instead.
Exercise
Add an "implies" function to the above Boolean expression calculator, using the
>
symbol to represent implication. You can look up K's builtin "implies"
function in the BOOL
module in domains.md
.
Integers in K
Unlike most programming languages, where the most basic integer type is a
fixedprecision integer type, the most commonly used integer sort in K is
the Int
sort, which represents the mathematical integers, ie,
arbitraryprecision integers.
K provides three main modules for import when using the Int
sort. The first,
containing all the syntax of integers as well as all of the functions over
integers, is the INT
module. The second, which provides just the syntax
of integer literals themselves, is the INTSYNTAX
module. However, unlike
most builtin sorts in K, K also provides a third module for the Int
sort:
the UNSIGNEDINTSYNTAX
module. This module provides only the syntax of
nonnegative integers, i.e., natural numbers. The reasons for this involve
lexical ambiguity. Generally speaking, in most programming languages, 1
is
not a literal, but instead a literal to which the unary negation operator is
applied. K thus provides this module to ease in specifying the syntax of such
languages.
For detailed information about the functions available over the Int
sort,
refer to domains.md
. Note again how we append Int
to the end of most of the
integer operations to ensure they do not collide with the syntax of other
programming languages.
Exercises

Extend your solution from lesson 1.4, problem 2 to implement the rules that define the behavior of addition, subtraction, multiplication, and division. Do not worry about the case when the user tries to divide by zero at this time. Use
/Int
to implement division. Test your new calculator implementation by executing the arithmetic expressions you wrote as part of lesson 1.3, problem 2. Check to make sure each computes the value you expected. 
Combine the Boolean expression calculator from this lesson with your solution to problem 1, and then extend the combined calculator with the
<
,<=
,>
,>=
,==
, and!=
expressions. Write some Boolean expressions that combine integer and Boolean operations, and test to ensure that these expressions return the expected truth value. 
Compute the following expressions using your solution from problem 2:
7 / 3
,7 / 3
,7 / 3
,7 / 3
. Then replace the/Int
function in your definition withdivInt
instead, and observe how the value of the above expressions changes. Why does this occur?
Next lesson
Once you have completed the above exercises, you can continue to Lesson 1.7: Side Conditions and Rule Priority.