Commit 1946789f authored by Sarah Grebing's avatar Sarah Grebing

Started with the Documentation

parent 2b127318
Pipeline #13524 failed with stage
in 2 minutes and 54 seconds
...@@ -24,7 +24,7 @@ name. Single '...'and double quotes "..." can both be used. ...@@ -24,7 +24,7 @@ name. Single '...'and double quotes "..." can both be used.
<br> <br>
Single-line comments are start with //. Single-line comments are start with //.
<h3>KeY Rules</h3> <h3>KeY Rules/Taclets</h3>
All KeY rules can be used as proof command. 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. 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 If no argument is following the proof command the taclet corresponding to this command has to match at most once on the
...@@ -78,10 +78,52 @@ inst_occ="..."). ...@@ -78,10 +78,52 @@ inst_occ="...").
</ul> </ul>
<h3>Macro-Commands</h3> <h3>Macro-Commands</h3>
In the KeY system macro commands are proof strategies tailored to specific proof tasks. In the KeY system macro commands are proof strategies tailored to specific proof tasks.
The available macro commands are listed below. Using them in a script is similar to using rule commands: The available macro commands can be found using the command help.
Using them in a script is similar to using rule commands:
<br> <br>
MACRONAME (PARAMETERS)? MACRONAME (PARAMETERS)?
<br> <br>
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>
<!-- <!--
......
...@@ -35,18 +35,30 @@ system for Java program annotated with the Java Modeling Language (JML). ...@@ -35,18 +35,30 @@ system for Java program annotated with the Java Modeling Language (JML).
<p> <p>
The protypical implementation includes a proof scripting language that is tailored to the The protypical implementation includes a proof scripting language that is tailored to the
problem domain of program verification. problem domain of program verification.
The language particualrily allows to: The main features of the language are:
<ol> <ol>
<li></li> <li> integration of domain specific entities like goal, formula, term and rule as
<li></li> first-class citizens into the language;</li>
<li></li> <li> an expressive proof goal selection mechanism
<li></li> <ul>
<li>to identify and select individual proof branches,</li>
<li>to easily switch between proof branches,</li>
<li>to select multiple branches for uniform treatment (multi-matching);</li>
</ul>
that is resilient to small changes in the proof</li>
<li> a repetition construct which allows repeated application of proof strategies;</li>
<li> support for proof exploration within the language.</li>
</ol> </ol>
Together with the proof scripting language a debugging concept for failed proof attempts Together with the proof scripting language a debugging concept for failed proof attempts
is implemented that leverages well-known concepts from program debugging to is implemented that leverages well-known concepts from program debugging to
the analysis of failed proof attempts. the analysis of failed proof attempts.
</p> </p>
<h2>Publications</h2>
A full description of the language and debugging-concept is published at <a href="">HVC 2017</a>.
<h2>Features</h2> <h2>Features</h2>
<div class="column"> <div class="column">
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment