From 1946789ffa982468aff3792417a6918a3e516bea Mon Sep 17 00:00:00 2001
From: Sarah Grebing <grebing@ira.uka.de>
Date: Mon, 11 Sep 2017 09:32:24 +0200
Subject: [PATCH] Started with the Documentation

---
 .../edu/kit/iti/formal/psdbg/gui/intro.html   | 46 ++++++++++++++++++-
 website/docs/index.md                         | 22 +++++++--
 2 files changed, 61 insertions(+), 7 deletions(-)

diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/intro.html b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/intro.html
index 6a231bcd..832cfecd 100644
--- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/intro.html
+++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/intro.html
@@ -24,7 +24,7 @@ name. Single '...'and double quotes "..." can both be used.
 <br>
 Single-line comments are start with //.
 
-<h3>KeY Rules</h3>
+<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
@@ -78,10 +78,52 @@ inst_occ="...").
 </ul>
 <h3>Macro-Commands</h3>
 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>
 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>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>
+
+
 <!--
 
 
diff --git a/website/docs/index.md b/website/docs/index.md
index 067037d5..d19ad0d4 100644
--- a/website/docs/index.md
+++ b/website/docs/index.md
@@ -35,18 +35,30 @@ system for Java program annotated with the Java Modeling Language (JML).
 <p>
 The protypical implementation includes a proof scripting language that is tailored to the
 problem domain of program verification.
-The language particualrily allows to:
+The main features of the language are:
 <ol>
-    <li></li>
-    <li></li>
-    <li></li>
-    <li></li>
+<li> integration of domain specific entities like goal, formula, term and rule as
+first-class citizens into the language;</li>
+<li> an expressive proof goal selection mechanism
+<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>
 Together with the proof scripting language a debugging concept for failed proof attempts
 is implemented that leverages well-known concepts from program debugging to
 the analysis of failed proof attempts.
+
 </p>
+<h2>Publications</h2>
+A full description of the language and debugging-concept is published at <a href="">HVC 2017</a>.
+
 <h2>Features</h2>
 
 <div class="column">
-- 
2.26.2