intro_old.html 9.15 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
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
77
78
79
80
81
82
83
84
85
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
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
<html>
<head>
    <title>Introduction to Proof Scripting Language for the KeY system</title>
    <meta content="">
    <style></style>
</head>
<body>
<h1>Language Constructs</h1>
This description is an adapted version of the README for script commands in KeY by Mattias Ulbrich.
<br>
Proof scripts are textual representations of rule applications,
settings changes and macro invocations.

<h2>Proof Commands</h2>

Proof commands start with an identifier followed by optional
arguments:
<br>
command argName="argument" "argument without name" ;
<br>
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.
<br>
Single-line comments are start with //.

<h3>KeY Rules/Taclets</h3>
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>

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="...").


<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"'

</ul>
<h3>Macro-Commands</h3>
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:
<br>
MACRONAME (PARAMETERS)?
<br>
Often used macro commands are:
<ul>
    <li>symbex : performs symbolic execution</li>
    <li>auto: invokes the automatic strategy of key</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>


<!--



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
addCell 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       updateTarget 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 addCell
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>
</html>