intro.html 9.19 KB
Newer Older
1 2 3 4 5 6
<html>
<head>
    <title>Introduction to Proof Scripting Language for the KeY system</title>
    <meta content="">
    <style></style>
</head>
7 8
<body>
<h1>Language Constructs</h1>
9
This description is an adapted version of the README for script commands in KeY by Mattias Ulbrich.
Sarah Grebing's avatar
Sarah Grebing committed
10
<br>
11
Proof scripts are textual representations of rule applications,
12
settings changes and macro invocations.
13

14
<h2>Proof Commands</h2>
15 16 17

Proof commands start with an identifier followed by optional
arguments:
18
<br>
19
command argName="argument" "argument without name" ;
20
<br>
21 22
Every command is terminated with a semicolon. There are named
arguments in the form argName="argument" and unnamed argument without
23 24 25
name. Single '...'and double quotes "..." can both be used.
<br>
Single-line comments are start with //.
26

Sarah Grebing's avatar
Sarah Grebing committed
27
<h3>KeY Rules/Taclets</h3>
28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43
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.
<br>
A rule command has the following syntax:<br>
RULENAME (on="TERM")? (formula="TOP_LEVEL_FORMULA")? (occ="OCCURENCE_IN_SEQUENT")? (inst_="TERM")? (maxSteps=INT)
<br>with:
<ul>
    <li>TERM: specific sub-term</li>
    <li>TOP_LEVEL_FORMULA: specific top level formula</li>
    <li>OCCURENCE_IN_SEQUENT: Number of occurence in the sequent</li>
    <li>maxSteps: the number of steps KEY should at most use until it terminateds teh proof search</li>
</ul>
44

45 46 47 48 49
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="...").
50 51


52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76
<h4>Examples</h4>
<ul>
    <li>andRight;</li>
    <br>
    Applicable iff there is only one matching spot on the sequent

    <li>eqSymm formula="a=b";</li>
    <br>
    This command changes the sequent "a=b ==> c=d" to "b=a ==> c=d"
    Using only "eqSymm;" alone would have been ambiguous.

    <li>eqSymm formula="a=b->c=d" occ=2;</li>
    <br>
    This command changes sequent "a=b->c=d ==>" to "a=b->d=c ==>".
    The occurrence number is needed since there are two possible applications on the formula

    <li>eqSymm formula="a=b->c=d" on="c=d";</li>
    <br>
    This command changes the sequent "a=b->c=d ==>" to "a=b->d=c ==>".
    It is simialr to the example above, but here the option to specify a
    subterm instead of an occurrence number is used.

    <li>cut cutFormula="x > y";</li>
    <br>
    This command is almost the same as 'cut "x>y"'
77

78 79
</ul>
<h3>Macro-Commands</h3>
80
In the KeY system macro commands are proof strategies tailored to specific proof tasks.
Sarah Grebing's avatar
Sarah Grebing committed
81 82
The available macro commands can be found using the command help.
Using them in a script is similar to using rule commands:
83 84 85
<br>
MACRONAME (PARAMETERS)?
<br>
Sarah Grebing's avatar
Sarah Grebing committed
86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126
Often used macro commands are:
<ul>
    <li>symbex : performs symbolic execution</li>
    <li>auto: invokes the automatic strategy of key</li>
    <li>heap_simp: performs heap simplification</li>
    <li>autopilot: full autopilot</li>
    <li>autopilot_prep: preparation only autopilot</li>
    <li>split_prop: propositional expansion w/ splits</li>
    <li>nosplit_prop: propositional expansion w/o splits</li>
    <li>simp_upd: update simplification</li>
    <li>simp_heap: heap simplification</li>

</ul>

Example:

auto;
<h2>Selectors</h2>
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 <em>cases</em>. Such a <em>cases</em>-statement has the following structure:
<br>
cases { <br>
case MATCHER: <br>
STATEMENTS <br>
[default: <br>
STATEMENTS]?<br>
}

<h2>Control Flow Statements</h2>
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.
<ul>
    <li>foreach {STATEMENTS}</li>
    <li>theOnly {STATEMENTS}</li>
    <li>repeat {STATEMENTS}</li>

</ul>


127
<!--
128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296



Commands in scripts
-------------------

This list of available script commands is subject to change and to
extension. If you write your own script commands (s. below), please
add an explanation to this list here. The list is sorted alphabetically.

-- auto ------------------

Apply the automatic KeY strategy on the current goal. Optinally you
can specify the number of steps to run.

Examples:
auto steps=30000;
# run at most 30000 steps automatically.

-- cut -------------------

Performs a cut and thus splits the sequent into two goals. The unnamed
argument is the formula to cut with

Examples:
cut "value1 = value2";

-- exit ------------------

Terminate the script prematurely at that point. Used mainly for debug
purposes.

Examples:
exit;

-- instantiate -----------

Quantifier instantiation is a task that often occurs. Instead of
specifying the entire formula, it suffices here to name the variable
that is to be instantiated. If that is not unique, the number of the
occurrence of that quantified variable can be specified as well.

Examples:
instantiate var="x" occ="3" with="42"
# Instantiate the third instantiateable formula whose bound
# variable is called "x" with the value 42

instantiate formula="\forall int x; f(x) = 42" with="23"
# The quantified formula can also be specified if wanted.
# This here for the antecedent.

instantiate formula="\exists int x; f(x) = 42" with="23"
# Existentially quantified variables can be instantiated if they
# occur on the succedent side.

instantiate hide var=x value="x_0"
# instantiate x and hide the quantified formula

-- leave -----------------

Mark the currently active goal as non-interactive (the orange hand
symbol in the GUI). It is then excluded from further analysis by
scripts. This is good for debugging unfinished proof scripts.

-- macro -----------------

Invoke a macro on the current goal. The names of available macros
include:

autopilot      full autopilot
autopilot-prep preparation only autopilot
split-prop     propositional expansion w/ splits
nosplit-prop   propositional expansion w/o splits
simp-upd       update simplification
simp-heap      heap simplification

Examples:
macro autopilot-prep;

(Future version may drop the macro keyword and allow macro invocations
directly.)

-- rule ------------------

Apply a single rule onto the current sequent. As unnamed argument add
the name of the taclet to be applied. If the taclet matches only once
on the entire sequent, the rule is applied. If it matches more than
once you need to specify more. In that case you can first specify the
sequence formula and then the number of the occurrence in the formula
or the specific subterm via the 'on' keyword.
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:
rule andRight;
# if there is only one matching spot on the sequent

rule eqSymm formula="a=b";
# changes sequent "a=b ==> c=d" to "b=a ==> c=d"
# "rule eqSymm;" alone would have been ambiguous.

rule eqSymm formula="a=b->c=d" occ=2;
# changes sequent "a=b->c=d ==>" to "a=b->d=c ==>".
# occurrence number needed since there are
# two possible applications on the formula

rule eqSymm formula="a=b->c=d" on="c=d";
# changes sequent "a=b->c=d ==>" to "a=b->d=c ==>".
# same as above, but using the option to specify a
# subterm instead of an occurrence number.

rule cut cutFormula="x > y";
# almost the same as 'cut "x>y"'

-- script ----------------

Invoke another script which resides in an external file.

Example:
script '/path/to/other/file.script';

-- select ----------------

Unlike most other commands, this command does not change the proof but
chooses the goal on which the next step operates. Currently you can
specify a formula. The goal is chosen such that the formula appears
(toplevel) on the sequent (antecedent or succedent). You can limit the
search to antecedent or succedent.

Examples:
select formula="{ x:=1 }y < x";
# search for the formula anywhere
select succedent formula="wellFormed(someHeap)";
# search only the succedent for the formula

-- smt -------------------

Invoke an external SMT solver. That solver must be adequately
configured outside the script mechanism. By default, Z3 is invoked,
but that can be chosen.

Examples:
smt;
# invoke Z3
smt solver="Z3,yices";
# a comma separated list of solvers can be specified.

-- tryclose --------------

Unlike other commands this command operates on ALL open goals and
effectively applies the "try provable goals below" macro to all of
them. A number of steps can optionally be given.

Examples:
tryclose;
tryclose steps=2000;
# spend 2000 steps on each open goal


Write your on proof commands
----------------------------

to be done.
Contact Mattias, if you are interested.
-->
</body>
297
</html>