Skip to content

GitLab

P
ProofScriptParser
Commit 4e279984 authored by Sarah Grebing's avatar Sarah Grebing
Browse files
Options

Documentation of both examples and webpage

parent 51ea4b27
Pipeline #17224 failed with stages
          in 118 minutes and 59 seconds
          Expand all Show whitespace changes
          Inline Side-by-side
          Showing with 554 additions and 273 deletions
          ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/help.html
          View file @ 4e279984
          ......@@ -2,7 +2,14 @@
          <body>
          <h1>Contraposition</h1>
          <p>To load a script it needs to be called in the main script.
          For example to load the script cpwob() type <i>cpwob;</i> in the body of the script <i> main()</i></p>
          For this right click to the scripts declaration and select "Set as Mainscript".
          </p>
          These example scripts are only for demonstration purposes,
          the underlying verification system just needs to be invoked with the automatic strategy "auto".
          This can be seen in the first script.
          The interactive script is to demonstrate the interactive rule applications.
          </body>
          </html>
          \ No newline at end of file
          ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/help.html 0 → 100644
          View file @ 4e279984
          <html>
          <body>
          <h1>Quicksort's split methods</h1>
          <p>This script is part of a case study to evaluate our language KPS. It is used to
          prove the Split method of a Quicksort implementation.</p>
          <p> This script is used to guide the proof for the method
          split() of a Quicksort implementation.</p>
          <p>In the first
          lines the proof state is pre-processed, i.e., the program is symbolically.
          The user is now left with a proof in which the proof goals each
          correspond a program state and a part of the proof obligation that needs to be shown for this path.
          For each of the more than 30 proof goals the next foreach block in the script invokes the
          prover's strategy tryclose, which tries to close the proof goal with built-in strategies or,
          if this is not successful, prunes the proof back to the goal the user has seen last.
          In the two remaining proof goals, it needs to be shown that during the
          loop execution the permutation property of the input array and the partial sorted array
          is preserved and
          that the loop invariant together with the rest of the program implies the post condition.
          To show that the permutation property holds, we make use of the taclet seqPermFromSwap:
          This taclet states that if we know that A is a permutation of B and we have to show that C is a permutation of D,
          then it suffices to prove that
          <ol>
          <li>B is equal to D</li>
          <li>and there exist two indices in A such that if the elements at these positions are swapped we obtain B.</li>
          </ol>
          The two proof obligations to show are added to the sequents suceedent and after applying the rule andRight
          four proof goals remain: two where we have to show case (1) and two where we have to show case (2).
          </p>
          <p> In the cases block, a distinction according to the shape of the proof
          obligation introduced by the seqPermFromSwap taclet is done and those proof branches that
          could be handled by the prover's auto strategy are captured by the first
          case. In the second case the prover needs guidance in the form of quantifier
          instantiations before it is able to find a proof.
          </p>
          </body>
          </html>
          \ No newline at end of file
          ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/intro_old.html 0 → 100644
          View file @ 4e279984
          <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>
          \ No newline at end of file
          website/docs/index.md
          View file @ 4e279984
          ......@@ -75,18 +75,81 @@ is published at [HVC 2017](http://rdcu.be/E4fF)
          ## Debugging Script for Quicksort's `split` method.
          ### Selecting the proof script
          <center>
          <video width="80%" controls>
          <source src="../psdbg_videos/selection.webm" type="video/webm">
          Your browser does not support the video tag.
          </video>
          </center>
          In this video the selection of the Quicksort example from the paper is shown.
          After loading the example a dialog appears in which the appropriate contract for the
          Java method `split` has to be selected. After loading the problem the program to be verified is
          shown in an own view on the right side, the script is shown on the left side and in the middle the proof obligation and the list of open goals is shown.
          Views can be selected and docked to other places on the screen.
          Please note that after a succesful loadthe statusbar indicates that the contract was loaded.
          ### Setting a breakpoint and starting the Interpreter
          <center>
          The video will be uploaded on 23th, January.
          <video width="80%" controls>
          <source src="../psdbg_videos/breakpoint.webm" type="video/webm">
          Your browser does not support the video tag or WebM.
          </video>
          </center>
          In this video it is shown how to set a breakpoint and how to start the debugger/interpreter. Please note that if no script is set as main script the first script in the open editor is taken as main script an set. This can be seen in the status bar.
          Furthermore the status of the interprter is shown with small icons in the right lower corner of the status bar. A running interpreter is indicated by a running figure. A paused interpreter is indicated by a timer.
          If the interpreter reaches the end of the proof script the status is shown as a tick.
          The video does not include the full execution until the breakpoint, as executing certain proof commands may take time.
          <!--
          ### Stepping into, over and reverse and continue
          <center>
          <video width="80%" controls>
          <source src="quicksort.webm" type="video/webm">
          <source src="../psdbg_videos/stepping_new.webm" type="video/webm">
          Your browser does not support the video tag or WebM.
          </video>
          -->
          </center>
          After reaching the breakpoint set in the video before, we are left with 4 open goals, visible in the goal list.
          In this video the stepping functionalities are demonstrated. Stepping into proof commands of the underlying verification system
          results in a view of the partial proof tree corresponding to the execution of this command.
          It can also be seen to which sequents the matching expression matches.
          ### Successful Proof Indication
          <center>
          <video width="80%" controls>
          <source src="../psdbg_videos/proof_new.webm" type="video/webm">
          Your browser does not support the video tag or WebM.
          </video>
          </center>
          In this video the successful proof is shown and it is demonstrated how to access the full proof tree of the proof for the `split` method.
          ### SequentMatcher and Interactive Rule Application
          <center>
          <video width="80%" controls>
          <source src="../psdbg_videos/interactive.webm" type="video/webm">
          Your browser does not support the video tag or WebM.
          </video>
          </center>
          In this video we demonstrate the interactive point and click rule applications after selecting the interactive button.We further demonstrate how the interaction is included to the original script.
          <center>
          <video width="80%" controls>
          <source src="../psdbg_videos/sequentmatcher.webm" type="video/webm">
          Your browser does not support the video tag or WebM.
          </video>
          </center>
          Furthermore, we show how to use our SequentMatcher Window to enhance the auto-generated matching expressions from the
          interactive rule applications.
          ## Features
          <div class="column">
          ......@@ -128,7 +191,7 @@ Your browser does not support the video tag or WebM.
          <div class="feature-caption">
          Stepwise script execution: step over and into.
          Our special offers for time travellers: Go backwards in time
          and then Back to the Future,again!
          and then Back to the Future, again!
          </div>
          </div>
          <div>
          ......@@ -145,8 +208,8 @@ Your browser does not support the video tag or WebM.
          <h2>Downloads</h2>
          <ul>
          <li>PSDBG - <strong>Version 1.0-FM will be available at 23th, January</strong>
          <a href="~/releases/psdbg-1.0-fm.jar">psdbg-1.0-fm.jar</a>
          <li>PSDBG - <strong>Version 1.0-FM</strong>
          <a href="../psdbg_releases/psdbg-1.0-fm.jar">psdbg-1.0-fm.jar</a>
          <br>
          Special Version for the tool paper at Formal Methods 2018.
          Including examples and all dependencies.
          ......
          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