Skip to content

P
ProofScriptParser
Commit 2b127318 authored by Alexander Weigl's avatar Alexander Weigl
Browse files
Options

website->mkdocs

parent 11b1f96d
Pipeline #13516 failed with stage
    in 3 minutes and 6 seconds
    Expand all Hide whitespace changes
    Inline Side-by-side
    Showing with 26081 additions and 0 deletions
    .gitignore
    View file @ 2b127318
    target/ target/
    *.iml *.iml
    .idea .idea
    website/site/
    website/docs/commands.md 0 → 100644
    View file @ 2b127318
    # Commands
    Generated on: Sat Sep 09 23:02:01 CEST 2017 by `gendoc.groovy`.
    Covering the macros of [KeY](http://key-project.org).
    # macro
    > Synopsis: `c.getName()) <STRING>`
    **Arguments:**
    * `#2` : *STRING* (*R*)
    # auto
    > Synopsis: `c.getName()) [all=<BOOLEAN>] [steps=<INT>]`
    **Arguments:**
    * `all` : *BOOLEAN*
    * `steps` : *INT*
    # cut
    > Synopsis: `c.getName()) <TERM>`
    **Arguments:**
    * `#2` : *TERM* (*R*)
    # set
    > Synopsis: `c.getName()) [oss=<BOOLEAN>]`
    **Arguments:**
    * `oss` : *BOOLEAN*
    # select
    > Synopsis: `c.getName()) formula=<TERM>`
    **Arguments:**
    * `formula` : *TERM* (*R*)
    # schemaVar
    > Synopsis: `c.getName()) <STRING> <STRING>`
    **Arguments:**
    * `#2` : *STRING* (*R*)
    * `#3` : *STRING* (*R*)
    # focus
    > Synopsis: `c.getName()) <SEQUENT>`
    **Arguments:**
    * `#2` : *SEQUENT* (*R*)
    # rule
    > Synopsis: `c.getName()) <STRING> [on=<TERM>] [formula=<TERM>] [occ=<INT>]`
    **Arguments:**
    * `#2` : *STRING* (*R*)
    * `on` : *TERM*
    * `formula` : *TERM*
    * `occ` : *INT*
    # skip
    > Synopsis: `c.getName())`
    **Arguments:**
    # instantiate
    > Synopsis: `c.getName()) formula=<TERM> var=<STRING> occ=<INT> with=<TERM>`
    **Arguments:**
    * `formula` : *TERM* (*R*)
    * `var` : *STRING* (*R*)
    * `occ` : *INT* (*R*)
    * `with` : *TERM* (*R*)
    # script
    > Synopsis: `c.getName()) <STRING>`
    **Arguments:**
    * `#2` : *STRING* (*R*)
    # javascript
    > Synopsis: `c.getName()) <STRING>`
    **Arguments:**
    * `#2` : *STRING* (*R*)
    # exit
    > Synopsis: `c.getName())`
    **Arguments:**
    # tryclose
    > Synopsis: `c.getName()) steps=<INTEGER> <STRING>`
    **Arguments:**
    * `steps` : *INTEGER* (*R*)
    * `#2` : *STRING* (*R*)
    # leave
    > Synopsis: `c.getName())`
    **Arguments:**
    # let
    > Synopsis: `c.getName())`
    **Arguments:**
    # smt
    > Synopsis: `c.getName()) solver=<STRING>`
    **Arguments:**
    * `solver` : *STRING* (*R*)
    # assume
    > Synopsis: `c.getName()) <TERM>`
    **Arguments:**
    * `#2` : *TERM* (*R*)
    website/index.html → website/docs/index.md
    View file @ 2b127318
    <html> <style>
    <head>
    <style>
    body {
    background: #333;
    font-family: sans-serif;
    font-size: 12pt;
    }
    #content { #content {
    width: 60em; width: 60em;
    ...@@ -27,61 +20,56 @@ ...@@ -27,61 +20,56 @@
    width: 150px; width: 150px;
    text-align: center; text-align: center;
    } }
    </style>
    <h1>Proof Script Debugger for the KeY System</h1>
    <p>The proof script debugger is a prototypical implementation
    of an interaction concept for program verification systems that are rule based and
    use a program logic.
    The prototype is implemented on top of the interactive program verification system
    <a href="http://www.key-project.org">KeY</a>. KeY is an interactive program verification
    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
    problem domain of program verification.
    The language particualrily allows to:
    <ol>
    <li></li>
    <li></li>
    <li></li>
    <li></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>Features</h2>
    <div class="column">
    <div >
    <img src="https://placeimg.com/150/150/any" />
    <h3>Feature 1</h3>
    <p>
    </p>
    </div>
    </style> <div >
    </head> <img src="https://placeimg.com/150/150/any" />
    <body> <h3>Feature 2</h3>
    <div id="content"> </div>
    <h1>Proof Script Debugger for the KeY System</h1>
    <p>The proof script debugger is a prototypical implementation
    of an interaction concept for program verification systems that are rule based and
    use a program logic.
    The prototype is implemented on top of the interactive program verification system
    <a href="http://www.key-project.org">KeY</a>. KeY is an interactive program verification
    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
    problem domain of program verification.
    The language particualrily allows to:
    <ol>
    <li></li>
    <li></li>
    <li></li>
    <li></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>Features</h2>
    <div class="column">
    <div >
    <img src="https://placeimg.com/150/150/any" />
    <h3>Feature 1</h3>
    <p>
    </p>
    </div>
    <div >
    <img src="https://placeimg.com/150/150/any" />
    <h3>Feature 2</h3>
    </div>
    <div >
    <img src="https://placeimg.com/150/150/any" />
    <h3>Feature 3</h3>
    </div>
    <div >
    <img src="https://placeimg.com/150/150/any" />
    <h3>Feature 3</h3>
    </div> </div>
    <div style="clear: both;"/>
    </div>
    <div style="clear: both;"/>
    <div class="column"> <div class="column">
    <div > <div >
    <img src="https://placeimg.com/150/150/any" /> <img src="https://placeimg.com/150/150/any" />
    ...@@ -105,22 +93,20 @@ ...@@ -105,22 +93,20 @@
    <div style="clear: both;"/> <div style="clear: both;"/>
    <!-- <h2>Getting Started</h2> <!-- <h2>Getting Started</h2>
    <h2>Downloads</h2> <h2>Downloads</h2>
    <ul> <ul>
    <li>Version 1.0 <li>Version 1.0
    <p> <p>
    <a href="#">psdb-0.9-alpha.jar</a> <a href="#">psdb-0.9-alpha.jar</a>
    </p> </p>
    </li> </li>
    </ul> </ul>
    --> -->
    <footer style="border-top: #ccc 1px solid"> <footer style="border-top: #ccc 1px solid">
    Contact: <a href="https://formal.iti.kit.edu/~grebing/">Sarah Grebing</a> Contact: <a href="https://formal.iti.kit.edu/~grebing/">Sarah Grebing</a>
    </footer> </footer>
    </p></div> </p>
    </body>
    </html>
    \ No newline at end of file
    website/docs/macros.md 0 → 100644
    View file @ 2b127318
    # Macros
    Generated on: Sat Sep 09 23:02:00 CEST 2017 by `gendoc.groovy`.
    Covering the macros of [KeY](http://key-project.org).
    ## Full Information Flow Auto Pilot (`infflow-autopilot`)
    Information Flow
    <html><ol><li>Search exhaustively for applicable position, then<li>Start auxiliary computation<li>Finish symbolic execution<li>Try to close as many goals as possible<li>Apply macro recursively<li>Finish auxiliary computation<li>Use information flow contracts<li>Try to close as many goals as possible</ol>
    ## Close provable goals below (`tryclose`)
    null
    Closes closable goals, leave rest untouched (see settings AutoPrune). Applies only to goals beneath the selected node.
    ## Update Simplification Only (`simp-upd`)
    Simplification
    Applies only update simplification rules
    ## Full Auto Pilot (`autopilot`)
    Auto Pilot
    <html><ol><li>Finish symbolic execution<li>Separate proof obligations<li>Expand invariant definitions<li>Try to close all proof obligations</ol>
    ## Finish symbolic execution (`symbex`)
    Auto Pilot
    Continue automatic strategy application until no more modality is on the sequent.
    ## Propositional expansion (w/ splits) (`split-prop`)
    Propositional
    Apply rules to decompose propositional toplevel formulas; splits the goal if necessary
    ## Heap Simplification (`simp-heap`)
    Simplification
    This macro performs simplification of Heap and LocSet terms.
    It applies simplification rules (including the "unoptimized" select rules), One Step Simplification, alpha, and delta rules.
    ## Auto pilot (preparation only) (`autopilot-prep`)
    Auto Pilot
    <html><ol><li>Finish symbolic execution<li>Separate proof obligations<li>Expand invariant definitions</ol>
    ## Propositional expansion (w/o splits) (`nosplit-prop`)
    Propositional
    Apply rules to decompose propositional toplevel formulas; does not split the goal.
    ## One Single Proof Step (`onestep`)
    Simplification
    One single proof step is applied
    website/docs/taclets.md 0 → 100644
    View file @ 2b127318
    This diff is collapsed.
    website/kit_theme/css/style.css 0 → 100644
    View file @ 2b127318
    This diff is collapsed.
    website/kit_theme/main.html 0 → 100644
    View file @ 2b127318
    This diff is collapsed.
    website/mkdocs.yml 0 → 100644
    View file @ 2b127318
    site_name: Proof Script Debugger -- KeY
    site_url: https://formal.iti.kit.edu/psdbg
    #weigl/verifaps/
    #repo_url: https://github.com/example/repository/
    site_description:
    site_author: Alexander Weigl <weigl@kit.edu>
    pages:
    - Home: index.md
    theme_dir: kit_theme
    markdown_extensions:
    - smarty
    - toc:
    permalink: True
    separator: "_"
    - sane_lists
    website/push.sh 0 → 100755
    View file @ 2b127318
    #!/bin/bash
    mkdocs build --clean
    rsync --delete -vr site/ i57adm.ira.uka.de:htdocs/grebing/psdbg/
    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