KORE Interface Design Rationale

** Under heavy construction. Do not read yet. **

(Rule 1) There is a main and an extended KORE interface. The main KORE interface changes only when the KORE language itself changes. The extended KORE interface can change occasionally, to provide useful utilities to front/back-ends.

(Rule 2) There is a bijective correspondence between the KORE language syntax and the main KORE interface. It should be trivial to translate between a textual KORE definition and its corresponding KORE interface variant.

(Rule 3) Clients of the main (but not the extended) KORE interface will never be affected by any changes to the extended KORE interface. In particular, the main KORE interface will not even be aware of names occurring in the extended KORE interface.

(Rule 4) The main KORE interface is split into extractors and builders. The builders

(R2) KORE faithfully captures the semantics of K.

(R3) KORE API should be minimal.

== Long Version ==

The KORE interface establishes a small set of requirements that any implementation of K must provide. There were several tensions in the design of the KORE interface.

On the one hand, we want it to be as faithful to the KORE language syntax as possible, so that users of the KORE language, or tools developed on top of the KORE language, can easily adapt to using the KORE API instead, programmatically. For example, if a static analysis tool decides to use K for symbolic execution or expression simplification, then it should be as easy for them to use the tool through the KORE API as it is to use, for example, an SMT solver through its API. On the other hand, for practical reasons we want it to provide as many services as possible to tool developers, in particular to our own team developing frontends and/or backends of K. Finally, the latter should not come at the expense of the former. That is, it is expected that users who want to take advantage of the additional services or data-structures have to face the additional complexity that comes with these, but users who are not interested in the extra features should not have to pay any extra price as an artifact of the extra features. Below we describe the rules that governed the design of the KORE API.

The main interface will only change if the KORE language syntax itself changes, which is expected to happen very rarely.

(R1) 1-to-1 correspondence between the KORE language and the main KORE API. We say main because, for practical reasons to better serve frontends and backends, the KORE API may also provide several other views (as ASTs with leaves and nodes with zero, one, two or more arguments, as binders vs. non-binders, etc.). However, a user who knows the KORE language should be able to easily develop parsers or pretty-printers to/from the KORE API, without having to understand more than the main API.

As an analogy, think of an SMT solver that offers both a textual interface to define specifications, say the smtlib2 standard, and an API for it. As a user of such an SMT solver, you expect the API to be in a 1-to-1 correspondence to the textual interface, so that you can easily switch from the textual interface that you used during experiments, to the API that you will ultimately use in you tool. Moreover, you would expect to get all the benefits of a good implementation of the API, that is: to add more constraints on the fly to take advantage of the incremental solving capability of the SMT, without having to resend the entire specification each time (which can be huge); and to extract data from the solution returned by the SMT by need, using the API, instead of getting the entire solution in a huge object (recall SMT formulae may have hundreds of thousands of variables).

How would you feel to have to be forced to first implement all sorts of auxiliary things ...

(R2) KORE faithfully captures the semantics of K. That is, any variant of K (read frontend) is expected to desugar to KORE without any semantic (including modularity) loss. The only acceptable loss is the concrete syntax convenience.

(R3) KORE API should be minimal. That is, users of it should not have to be aware of any artifacts of particular uses of KORE, such as of potential backends. For example, specific fields in (enriched) KORE data-structures used by (some, or our) backends to more efficiently have access to information specific to their needs, should not be exposed in the API.

As an analogy, consider the case of an SMT solver. As a user of (an API of) it, all you need to know is how to interact with it: build formulae, invoke the solver, extract data from the solution (without unnecessarily getting the entire solution, which can be huge), add more constraints, invoke the solver again incrementally, extract more data from the new solution, etc. You do not care about how the SMT solver enriches its API with internal fields/methods/constructors or data-structures, or if it even implements completely different data-structures that have nothing to do with the API (the so-called smtlib).

Similarly, users of the KORE API should have a minimal interface that they need to be aware of, and be protected from seeing any irrelevant details that have no immediate correspondence with the mathematical definition of K (KORE).