Tagging; Transition Kompilation Option
In this lesson we add the semantics of variable increment. In doing so, we
learn how to tag syntactic constructs and rules and then use such tags to
kompile tool to generate the desired language model that is
amenable for exhaustive analysis.
The variable increment rule is self-explanatory:
rule <k> ++X => I +Int 1 ...</k> <env>... X |-> N ...</env> <store>... N |-> (I => I +Int 1) ...</store>
We can now run programs like our
div.imp program introduced in Lesson 1.
The addition of increment makes the evaluation of expressions have side
effects. That, in combination with the non-determinism allowed by the
strictness attributes in how expression constructs evaluate their
arguments, makes expressions in particular and programs in general have
non-deterministic behaviors. One possible execution of the
y's location, for example, but this program manifests several
other behaviors, too.
To see all the (final-state) behaviors that a program can have, you can call
krun tool with the option
--search. For example:
krun div.imp --search
Oops, we see only one solution, the same as when we ran it without search.
Here is what happens.
krun can only explore as much of the transition
system associated to a program as
kompile allowed the generated language
model to yield. Since most of the K users are interested in language models
that execute efficiently, that is, in faster interpreters for the defined
languages, by default
kompile optimizes the generated language model for
execution. In particular, it inserts no backtracking markers, which
uses when called with the
--search option in order to systematically generate
the entire transition system associated to a program. This is why
showed us only one solution when run with the
--search option on
We next explain how to tell
kompile what kind of language model we are
interested in for analysis purposes. When you experiment with non-determinism
in a language semantics, you should keep it in mind that the
kompile allows you to configure what counts as a transition in
your language model. We here only discuss transitions due to the
non-deterministic evaluation strategies of language constructs, but we will
see in future lectures (see Lesson 6 of IMP++, where we add concurrency) that
we can also have transitions due to non-deterministic applications of rewrite
If you want to explore the entire behavior space due to non-deterministic
evaluation strategies, then you should include all the language constructs
--transition option. This may sound like the obvious thing to
always do, but as soon as you do it you soon realize that it is way too much
in practice when you deal with large languages or programs. There are simply
too many program behaviors to consider, and
krun will likely hang
on you or crush. For example, a small ten-statement program where each
statement uses one strict expression construct already has 1000+ behaviors for
krun to explore! Driven by practical needs of its users, the K tool
therefore allows you to finely tune the generated language models using the
To state which constructs are to be considered to generate transitions in the
generated language model, and for other reasons, too, the K tool allows you to
tag any production and any rule. You can do this the same way we tagged
rules with the
structural keyword in earlier tutorials: put the tag in
brackets. You can associate multiple tags to the same construct or rule, and
more than one construct or rule can have the same tag. As an example, let us
tag the division construct with
division, the lookup rule with
the increment rule with
increment. The tags of the rules are not needed
in this lesson, we do it only to demonstrate that rules can also be tagged.
The least intrusive way to enforce our current language to explore the
entire space of behaviors due to the strictness of division is to
with the following option:
kompile imp.k --transition "division"
It is interesting to note that the
increment rules are the only
two rules which can trigger non-deterministic behaviors for division, because
no other rule but these two can ever apply while a division operation is
heated. Previous versions of K allowed you to also specify which rules could
trigger non-deterministic behaviors of operator evaluation strategies,
but that option was rarely used and is not available anymore.
Note that it is highly non-trivial to say precisely whether a strict language construct may yield non-deterministic behaviors. For example, division's strictness would yield no non-determinism if the language had no side effects. It is even harder to say so for a particular program. Consequently, our K implementation makes no attempt to automatically detect which operations should be tagged as transitions. Instead, it provides the functionality to let you decide it.
Now the command
krun div.imp --search
shows us all five behaviors of this program. Interestingly, one of the five behaviors yields a division by zero!
--transition option can be quite useful when you experiment with your
language designs or when you formally analyze programs for certain kinds of
errors. Please let us know if you ever need more finer-grained control over
the non-determinism of your language models.
Before we conclude this lesson, we'd like to let you know one trick, which
you will hopefully not overuse: you can tag elements in your K definition with
kompile option names, and those elements will be automatically included in
their corresponding options. For example, if you tag the division production
transition then the command
is completely equivalent to the previous
Please use this default behavior with caution, or even better, try to avoid
using it! You may be tempted to add the
transition tag to lots of elements
and then forget about them; your language models will then be increasingly slower
when you execute them and you may wonder why ... This convention is typically
convenient when you want to quickly experiment with non-determinism and do not
want to bother inventing tag names and calling
kompile with options.
In the next lesson we add input/output to our language and learn how to generate a model of it which behaves like an interactive interpreter!