K Debugger

Current Status

Currently K has a textual debugger, which has the following functionality:

• Stepping - Step by step execution is supported. The initial and subsequent configurations are displayed. User can specify the number of steps that should be taken.

• Subsequent States - All possible states that can be reached from a particular state. Another state can be selected from these states for further execution. Thus, any branch of the execution tree can be explored.

Future Direction

The debugger is expected to be more than a concrete configuration stepper, and will eventually be an interactive program verifier.

Design Overview

The debugger will consists of one main API, which will interact with the broader Rewrite Engine's API.

Rewrite Engine API

This is the API by which the K framework tools make use of the rewrite engine provided by a backend. We want this API to be minimal and efficient. For example, an interface providing only a one-step rewrite relation is minimal but not efficient.

Debugger API

This is the API by which various debugger instances can access the state of the debugger.

Intended Functionality

• The debugger interface will allow for viewing of relevant parts of the configuration only. Sometimes, when configurations are very long, it's not feasible to view and find faults in the configuration. Hence, the debugger will allow for only parts of the configuration to be view (perhaps only the top cell initially). The user can then view the remaining parts of the configuration by clicking/selecting (depending on the interface) the part of the configuration required. (Also, it can be the case that the configuration's expansion/contraction will be managed by the fronted/observer, while the debugger will only manage the main rewriting functionality).

• The debugger will work with symbolic configurations as well.