KIT Logo - Link to KIT start page

Application-oriented Verification
Karlsruhe Institute of Technology

Language Constructs

Proof scripts are textual representations of rule applications, settings changes and strategy invocations (in the case of KeY as underlying verification system also referred to as macros).

Variables and Types

We need to distinguish between: logic, program, and script variables.

Proof Script Language has script variables.

A script variable has a name, a type and a value. Variables are declared by

var0 : type;
var1 : type :=  value;
var2 :=  value;

Both statements declare a variable, in the latter case (var1 and var2) we directly assign a value, in the first form var0 receives a default value.

Types and Literals

We have following types: INT, TERM<Sort>, String.

`f(x)` `g(a)` `imp(p,q)`

"i am a string"

Special Variables

To expose settings of the underlying prover to the user we include special variables:

Proof Commands

Proof commands start with an identifier followed by optional arguments:

command argName="argument" "positional argument" ;

Every command is terminated with a semicolon. There are named arguments in the form argName=”argument” and unnamed argument without name. Single '...' and double quotes "..." can both be used.

Single-line comments are start with //.

KeY Rules/Taclets

All KeY rules can be used as proof command. The following command structure is used to apply single KeY rules onto the sequent of a selected goal node. If no argument is following the proof command the taclet corresponding to this command has to match at most once on the sequent.

If more terms or formulas to which a proof command is applicable exist, arguments have to be given that indicate the where to apply the rule to.

A rule command has the following syntax:

RULENAME [on=TERM]?
         [formula=TERM]
         [occ=INT]
         [inst_*=TERM]

with:

If a rule has schema variables which must be instantiated manually, such instantiations can be provided as arguments. A schema variable named sv can be instantiated by setting the argument sv=”…” or by setting inst_sv=”…” (the latter works also for conflict cases like inst_occ=”…”).

Examples

Applicable iff there is only one matching spot on the sequent

This command is almost the same as cut \x>y``

Macro-Commands

In the KeY system macro commands are proof strategies tailored to specific proof tasks. The available macro commands can be found using the command help. Using them in a script is similar to using rule commands:

MACRONAME (PARAMETERS)?

Often used macro commands are:

Example:

auto;

Selectors

As nited before proof commands are implemented as single goal statements. Some proof commands split a proof into more than one goal. To allow to apply proof commands in proof state with more than one proof goal, the language allows for a selector statement cases. Such a cases-statement has the following structure:
cases {
case MATCHER:
STATEMENTS
[default:
STATEMENTS]?
}

Control Flow Statements

The script language allows different statements for control-flow. Control-Flow statements define blocks, therefor it is neccessary to use curly braces after a control-flow statement.