diff --git a/.gitignore b/.gitignore index 640f75b..0e9e8c2 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,5 @@ site/ +/public .DS_Store *.out diff --git a/Makefile b/Makefile index 76d8e9c..171d1cf 100644 --- a/Makefile +++ b/Makefile @@ -1,5 +1,5 @@ prepare: - pip install --user mkdocs mkdocs-material pymdown-extensions pygments markdown-blockdiag mkdocs-bibtex markdown-aafigure==v201904.0004 mkdocs-build-plantuml-plugin 'Pillow<10' 'Markdown<3.4' + pip install --user mkdocs mkdocs-material pymdown-extensions pygments markdown-blockdiag mkdocs-bibtex markdown-aafigure==v202104.1011 mkdocs-build-plantuml-plugin Pillow Markdown serve: mkdocs serve diff --git a/README.md b/README.md index ee1f72a..abdd7da 100644 --- a/README.md +++ b/README.md @@ -40,8 +40,8 @@ Install the necessary libraries locally: ``` $ pip install --user mkdocs mkdocs-material pymdown-extensions pygments \ - markdown-blockdiag mkdocs-bibtex markdown-aafigure==v201904.0004 \ - mkdocs-build-plantuml-plugin 'Pillow<10' 'Markdown<3.4' + markdown-blockdiag mkdocs-bibtex markdown-aafigure==v202104.1011 \ + mkdocs-build-plantuml-plugin Pillow Markdown ``` You can start development web-server, which automatically rerender and refresh diff --git a/docs/changelog.md b/docs/changelog.md index db367dd..ecc8657 100644 --- a/docs/changelog.md +++ b/docs/changelog.md @@ -1,5 +1,36 @@ # Changelog +## [2.12.2](https://github.com/KeYProject/key/releases/tag/KeY-2.12.2) (2023-11-10) +This release contains bug fixes and performance enhancements. + +### Performance: + - Z3 is now configurable to use the QF (quantifier-free) theory for problems without quantifiers. + +### Bug Fixes: + - The pretty printer no longer throws a ClassCastException when printing taclets using schema variables of an array type. + - Nullable and non-null modifiers attached to model methods are no longer lost. + - Term rule indices are now always up-to-date, preventing potential prover crashes. + - The counter-example dialog no longer freezes the GUI, if the example generation fails. + - The actual proof status and proof status icon in the task overview are now consistent after pruning without requiring a manual refresh. + +## [2.12.1](https://github.com/KeYProject/key/releases/tag/KEY-2.12.1) (2023-10-13) + +### Bug fixes + +- SMT solvers are properly terminated on timeout +- Proof Macro statistics are kept visible and only count the newly applied rules +- Stop button is disabled after use, re-enabled after stop completes (this is to avoid double activation) +- Fully disable origin tracking if it is disabled +- Proof slicing works even if a cut introduced no new formulas in any branch +- When marking goal(s) as interactive/automatic, proof tree no longer loses expansion state +- Fix proof tree behaviour when toggling goals +- Fix branch selection in caching +- Fix gradle detection of git branch +- Fix unit test +- Fix environments not disposed in tests, keep strategy info visible after applying +- Proof macro: record statistics correctly +- Fix: KeY files with errors cannot be edited + ## [2.12.0](https://github.com/KeYProject/key/releases/tag/KeY-2.12.0) (2023-08-18) ### Breaking changes @@ -14,8 +45,8 @@ * [Support for floating points](https://git.key-project.org/key/key/-/merge_requests/403) * [Support for JML asserts/assumes as standalone construct (instead of transforming into blockcontracts)](https://git.key-project.org/key/key/-/merge_requests/494), [Support of \old() in JML asserts](https://git.key-project.org/key/key/-/merge_requests/533) * [Support for JML math mode specifiers (and changed default semantics to spec_bigint_math)](https://github.com/KeYProject/key/pull/3014) -* [Proof Slicing](user/ProofSlicing.md) system ([#3026](https://github.com/KeYProject/key/pull/3026)) -* [Proof Caching](user/ProofCaching.md) system +* [Proof Slicing](../user/ProofSlicing/) system ([#3026](https://github.com/KeYProject/key/pull/3026)) +* [Proof Caching](../user/ProofCaching/) system * [Run the Javac compiler when loading Java code](https://git.key-project.org/key/key/-/merge_requests/581) * Migration to GitHub * [Files for Github Actions](https://git.key-project.org/key/key/-/merge_requests/634) diff --git a/docs/devel/How2ExtRecoder.md b/docs/devel/How2ExtRecoder.md index 99b3361..c7c5cb4 100644 --- a/docs/devel/How2ExtRecoder.md +++ b/docs/devel/How2ExtRecoder.md @@ -1,10 +1,10 @@ # How to extend recoder -*Schmitt, XXXX* +*Schmitt* -!!! abstract +!!! danger - Here should be a short abstract. + Recoder is planned to be removed. See [PR #3120](https://github.com/KeYProject/key/pull/3120). These notes explain the changes to the existing code of the KeY system that are necessary to add a new data type to JML. If the new data type is only used in diff --git a/docs/user/HowToTaclet.md b/docs/devel/HowToTaclet.md similarity index 97% rename from docs/user/HowToTaclet.md rename to docs/devel/HowToTaclet.md index 9e63f1e..d7997f5 100644 --- a/docs/user/HowToTaclet.md +++ b/docs/devel/HowToTaclet.md @@ -1,4 +1,4 @@ -# How to write a Taclet +# How to write new taclets New prover rules in KeY can be added in form of built-in rules[^1] written in plain Java code and as so-called "taclets" ("schematic theory-specific rules"). @@ -8,15 +8,14 @@ schematic parts are displayed to the user, making the rule application more transparent. Almost all rules implemented for KeY are defined as taclets (with the exception of special rules like method contract application, loop invariant application (so far) and one-step-simplification). For information about -taclets, please consult the [book chapter "Proof Search with -Taclets"](https://link.springer.com/chapter/10.1007/978-3-319-49812-6_4) of the +taclets, please consult the [book chapter "Proof Search with Taclets"](https://link.springer.com/chapter/10.1007/978-3-319-49812-6_4) of the 2nd KeY book. This article covers the necessary basics for adding new taclets to the KeY system. In particular, the following topics are discussed: -## How to add new taclets +## How to add a taclet The standard location for `.key` files containing taclets is in the `key.core` project, location `resources/de/uka/ilkd/key/proof/rules` (*note*: unless stated @@ -39,6 +38,10 @@ heuristics. Default rule sets are defined in the file ## How to extend the taclet language +!!! danger + + This section does not reflect recent KeY developments. [The parser was recently rewritten](../../devel/NewKeyParser/). + Sometimes, especially when one wants to introduce new symbolic execution concepts, the existing taclet language is not expressive enough and has to be extended. There are four things one might have to extend to support new taclet diff --git a/docs/devel/HowtoTaclet.md b/docs/devel/HowtoTaclet.md deleted file mode 100644 index 5dd07dc..0000000 --- a/docs/devel/HowtoTaclet.md +++ /dev/null @@ -1,238 +0,0 @@ -# Writing Taclets - -New prover rules in KeY can be added in form of built-in rules1 written in -plain Java code and as so-called "taclets" ("schematic theory-specific -rules"). Taclets permit for an easy-readable definition of rules; when -a taclet is applied during a proof, the taclet itself as well as the -instantiation of its schematic parts are displayed to the user, making -the rule application more transparent. Almost all rules implemented -for KeY are defined as taclets (with the exception of special rules -like method contract application, loop invariant application (so far) -and one-step-simplification). For information about taclets, please -consult the [book chapter "Proof Search with -Taclets"](https://link.springer.com/chapter/10.1007/978-3-319-49812-6_4) -of the 2nd KeY book. - -This article covers the necessary basics for adding new taclets to the -KeY system. In particular, the following topics are discussed: - - -### How to add new taclets - -The standard location for `.key` files containing taclets is in the -`key.core` project, location `resources/de/uka/ilkd/key/proof/rules` -(*note*: unless stated otherwise, all locations in this article are -relative to `key.core`). The file `standardRules.key` lists all the -taclet files that are are loaded as defaults when starting KeY with -the Java profile. New taclets can be added to either of the existing -files listed there (if they fit into the scope), or can be added to a -new file which is then referred to in `standardRules.key`. - -The standard rule file can be obtained from a profile -(`de.uka.ilkd.key.proof.init.Profile`) via the method -`getStandardRules()`. The class -`de.uka.ilkd.key.proof.init.JavaProfile`, for example, sets the -standard rules to the aforementioned `standardRules.key`. If one -wishes to add taclets that are unrelated to Java, that taclet should -be referred to from the standard rules collection of an appropriate -profile. - -Taclets can be added to "rule sets" which are used, e.g., by strategy -heuristics. Default rule sets are defined in the file -`resources/de/uka/ilkd/key/proof/rules/ruleSetDeclarations.key`. - -### How to extend the taclet language - -Sometimes, especially when one wants to introduce new symbolic -execution concepts, the existing taclet language is not expressive -enough and has to be extended. There are four things one might have to -extend to support new taclet features: (1) The taclet parsers; this -includes the parser for the taclet language itself (which usually will -not have to be changed) and the parser for new program constructs, (2) -for matching different classes of statements, corresponding model -classes will have to be added to the system, which are then referred -to in factory classes and the parser(s), (3) whenever the standard -find-replace pattern of taclets is not sufficient, one can add -"transformers" performing more complex actions during taclet -execution, and (4) when taclets depend on additional input such as -specifications, one can define (automatic or interactive) completions -for the taclet. We'll discuss all those points in the following. - -It might be helpful to (additionally?) learn about the process by -examples. To get started, an example for a new program statement used -for matching is "merge_point", the keyword for a merge point -statement. A simpler one is "ForLoop", a schema variable matching for -loops. If you search for those identifiers in all files in the -"key.core" project, you'll find the entry points needed for -extensions. Note that merge points are also used in JML -specifications, which is a different topic (therefore, you might want -to ignore the corresponding parser files "KeYJMLPre{Lexer, Parser}.g, -basically everything in the `(...)/speclang/jml` directory.). An -example for a transformer is the "#for-to-while" construct which -accepts a for loop as input and transforms it to a while loop. Your -friends here are the eclipse functionalities `Search -> File` (use -`*.*` as a pattern here, and only search in the key.core project), -`Ctrl+T` for finding types, and `Ctrl+R` for finding resources. - -#### Parsing - -There are several relevant parsers you might need to know. The "main -KeY parser", `src/de/uka/ilkd/key/parser/KeY{Lexer, Parser}.g` is an -ANTLR3 parser which covers KeY's language for sorts, terms, formulas -etc., taclets, and proof files. For most extensions, this file does -not need to be touched. - -The parsers for Java extensions in taclets and proof files are -`src/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj` and -`src/de/uka/ilkd/key/parser/schemajava/ProofJavaParser.jj`, which are -JavaCC parsers. In the former, you also find definitions for -`#for-to-while` and `merge_point`; in the latter, only `merge_point` -occurs since it is an extension of Java and not a transformer like -`#for-to-while` which is only needed in taclets, but will never occur -in a Java program. - -So, if for your taclet the basic taclet language has to be changed, -adapt `KeYParser.g` accordingly; for creating new transformers, -`SchemaJavaParser.jj` is the relevant parser, and for additions to the -Java language accepted by KeY, `SchemaJavaParser.jj` and -`ProofJavaParser.jj` will have to be changed. The best advice here is -to have a look at the existing definitions to see how to add a new -one. Note that at the same time when extending the parser by new -transformers or statement types, you will also have to add new Java -classes and extend factories. We cover this in the next section. - -#### New Program Statement / Expression Types - -There are two categories of extensions: (1) New program schema -variable sorts, which match existing programming language fragments, -and (2) extensions to the language, e.g. by artificial constructs -needed for a proof / symbolic execution technique. - -A new "matcher sort" for taclets is added quite easily. As an example, -take the "loop init" clause of a for loop. A corresponding schema -variable for the use in taclets can be declared as `\program LoopInit #loopInit;`. -After that, `#loopInit` can be used in a taclet to match -a loop init clause. It suffices to (1) declare a new "program schema -variable sort" in `de.uka.ilkd.key.logic.sort.ProgramSVSort` (for -instance `LoopInitSort` in the example) which calls the constructor of -`ProgramSVSort` with the identifier by which it later should be -referred to in taclet definitions, and (2) to use that sort in -`SchemaJavaParser.jj`. Have a look how `ForInit` is used there to get -a feeling. - -A language extension like the merge points has to be added to several parts in the system: - -1. A parser model extension is added in - `src/de/uka/ilkd/key/java/recoderext/` (see - `MergePointStatement.java` for an example). -2. The factories - `de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java` and - `(...)/ProofJavaProgramFactory.java` are extended by corresponding - factory methods. -3. A mirror of the parser extension for the logic side of KeY is added - to `de/uka/ilkd/key/java/statement/` (also here, there's a - `MergePointStatement.java`). -5. A converter for the parser model extension to the logic - representation in `de/uka/ilkd/key/java/Recoder2KeYConverter.java`. - Look what's done for the `MergePointStatement`. The methods there - are called by reflection, so the name of the new method has to be - `convert`, and it has to accept the parser model extension as only - argument. -6. Extension of Java visitor classes: Classes `Visitor.java`, - `JavaASTVisitor.java`, `CreatingASTVisitor.java`, and - `ProgVarReplaceVisitor.java` in directory - `de/uka/ilkd/key/java/visitor/`. Note that now all of these might - apply to you, e.g. if your new statement does not contain program - variables that might have to be substituted in a proof. -7. Extension of the pretty printer to nicely render your extension in - sequents: `de/uka/ilkd/key/java/PrettyPrinter.java`. - -The factory methods and parser model classes can then be used in -`{Schema, Proof}JavaParser.jj`. - -#### New Meta Constructs / Transformers - -Meta constructs give additional powers to taclets. By them, it is even -possible to create taclets which are actually built-in rules since all -the work (maybe except for some matcher preprocessing) is deferred to -a powerful transformer. Note that we discourage from using that style; -meta constructs should be used at a very small scope. If that's not -possible, directly using built-in rules is a more "honest" and better -maintainable approach. - -Our running example here is the `#for-to-while` construct (actually an -example for the bad style of delegating everything to a transformer). -For adding transformers this to the system, follow these steps: - -1. Add a model class to the directory - `src/de/uka/ilkd/key/rule/metaconstruct/` (see e.g. - `ForToWhile.java). The class should extend `ProgramTransformer` and - pass the keyword to be used to the super class, here - "#for-to-while". -2. Extend the class - `src/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter` to return the - new class when appropriate. Look for `convert(RKeYMetaConstruct)` - to see what's done for `#for-to-while`. -3. Add the construct to the parser (`SchemaJavaParser.jj`). - -#### Completions - -Sometimes the input to a taclet depends on other information than that -available from a current proof situation (i.e., a sequent). In that -case, the rule has to be completed before it is applied. A good -example is the rule "cut" -(`resources/de/uka/ilkd/key/proof/rules/propRule.key`) defined as -follows: - -``` -\schemaVariables { - \formula cutFormula; -} -cut { "CUT: #cutFormula TRUE":\add (cutFormula ==>); - "CUT: #cutFormula FALSE":\add (==> cutFormula) - \heuristics(cut) }; -``` - -The formula `cutFormula` is not obtained from the sequent, it's left -as a "hole" in the definition. When applying the rule in KeY, a -standard dialog will pop up asking for an instantiation of -"curFormula". - -For certain situations, special completions are required. A classic -example are rules depending on specification, like loop invariant or -method contract rule applications. To this end, custom completions -implementing -`/key.ui/src/de/uka/ilkd/key/gui/InteractiveRuleApplicationCompletion.java` -(note: this class is the first not residing in the key.core project) -can be added and registered in -`/key.ui/src/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java`. - -**NOTE/WARNING**: Obviously, interactive rule application completions -are currently only designed to handle BuiltInRules. So for taclets, -this will have to be adapted! - -Alternatively to the implementation of an interactive completion, -additional information, like for instance a specification, could be -retrieved by special meta constructs. Specifications are stored in -`de.uka.ilkd.key.proof.mgt.SpecificationRepository` and can be -retrieved via a call like -`services.getSpecificationRepository().getLoopSpec(loop)`. If the -specification repository already contains the means to store that -specification, this should be quite straightforward to accomplish. - ---- - -

  1. Built-in rules -reside in the directory src/de/uka/ilkd/key/rule/ and -implement the interface BuiltInRule. This simple -interface defines three methods only; however, when implementing -built-in rules, there are quite some things to consider, which are not -in the scope of this article. New BuiltInRules have to be registered -in the Profile they belong to, see -src/de/uka/ilkd/key/proof/init/JavaProfile.java, method -initBuiltInRules() for the place where BuiltInRules are -registered in the default Java profile. ↩

diff --git a/docs/devel/Listeners.md b/docs/devel/Listeners.md index c7442a6..b79e7f2 100644 --- a/docs/devel/Listeners.md +++ b/docs/devel/Listeners.md @@ -47,7 +47,7 @@ When in "auto mode", the KeY interface (except for the stop button) will not res ### InteractionListener -Listener for interactions done by the user: settings changed, macro started, rule applied, ... +Listener for interactions done by the user: settings changed, macro started, rule applied, proof pruned, ... ## Proof @@ -103,4 +103,4 @@ Receives an event whenever a value in the Lookup instance changes. ### MergeRuleProgressListener -When applying a merge rule, this listener will be notified for each merged branch. \ No newline at end of file +When applying a merge rule, this listener will be notified for each merged branch. diff --git a/docs/devel/NewKeyParser.md b/docs/devel/NewKeyParser.md index 8ce7581..01c8341 100644 --- a/docs/devel/NewKeyParser.md +++ b/docs/devel/NewKeyParser.md @@ -10,7 +10,7 @@ ## Background -With the MR !278, a new lexer and parser for the KeY language is introduced. The KeY language is used to parse the `*.key` and `*.proof`, and is also used as the input language for entering terms in the user interface. +With the MR [!278](https://git.key-project.org/key/key/-/merge_requests/278), a new lexer and parser for the KeY language is introduced. The KeY language is used to parse the `*.key` and `*.proof`, and is also used as the input language for entering terms in the user interface. In general, this parser was hard to maintain and extend over the years. The old parser was a traditional ANTLR3 parser, where the grammar and the source code are mixed up. It also some lookahead were required. KeY files are interpreted on different levels: The first level are the basic notions (e.g. sorts and choice options), second level are the functions, predicates and transformers, and the third level are the axioms, contracts and rules. These parsing level are required due to the dependencies between these logical entities, e.g. a rule requires certain functions and sorts during its interpretation. In the old KeY-Parser, each file is parsed (and read) on a specific level. Hence, to interpret a KeY file, multiple parse passes are required. diff --git a/docs/devel/Testing/RunAllProves.md b/docs/devel/Testing/RunAllProves.md index 7cd4228..80c4bdb 100644 --- a/docs/devel/Testing/RunAllProves.md +++ b/docs/devel/Testing/RunAllProves.md @@ -56,6 +56,10 @@ test runs. ### Syntax of the Proof Collection/Index File +!!! danger + + This section does not reflect recent KeY developments. In particular, this list is now defined in code. + There is an proof collection (or index) file containing the declaration the sets of .key files that will be tested during RunAllProofs test run. This file is currently located in KeY diff --git a/docs/devel/Testing/deterministicTestOrder.md b/docs/devel/Testing/deterministicTestOrder.md index c2732d6..da5d5f7 100644 --- a/docs/devel/Testing/deterministicTestOrder.md +++ b/docs/devel/Testing/deterministicTestOrder.md @@ -1,5 +1,9 @@ # Deterministic Order of Test Cases in KeY +!!! danger + + This section does not reflect recent KeY developments. In particular it no longer applies since the upgrade to JUnit 5. + In KeY, some test cases rely on a specific execution order. One reason for this may be for example that it is too expensive to always initialize a new ProofEnvironment and therefore the environment is shared between multiple test cases. To get rid of test cases failing due to wrong order, we implemented a solution to make the execution order of JUnit tests deterministic: A custom JUnit test runner called AutoSuite. diff --git a/docs/devel/howtodoc/index.md b/docs/devel/howtodoc/index.md index 580c6df..2378a5f 100644 --- a/docs/devel/howtodoc/index.md +++ b/docs/devel/howtodoc/index.md @@ -21,8 +21,8 @@ use either `make prepare` or execute the following line: ``` {.sh linenums="1"} $ pip install --user mkdocs mkdocs-material pymdown-extensions pygments \ - markdown-blockdiag mkdocs-bibtex markdown-aafigure==v201904.0004 \ - mkdocs-build-plantuml-plugin 'Pillow<10' 'Markdown<3.4' + markdown-blockdiag mkdocs-bibtex markdown-aafigure==v202104.1011 \ + mkdocs-build-plantuml-plugin Pillow Markdown ``` This install all needed packages for this webpage inside diff --git a/docs/devel/index.md b/docs/devel/index.md index 3e458dd..a83d6e0 100644 --- a/docs/devel/index.md +++ b/docs/devel/index.md @@ -7,17 +7,17 @@ - [Formatting Conventions](SpotlessAutomaticFormatting/) - [Gradle](Gradle/) - [Logging](Logging/) +- [Documentation](howtodoc/) ### Dependencies KeY uses the [Docking Frames](https://docking-frames.org/download.html) library to organize its UI. -If you wish to inspect the source code of DF classes in your IDE, you need to download and add the source code manually. ### Important topics - [GUI extensions](GUIExtensions/) - [Event listeners](Listeners/) -- [Writing Taclets](HowtoTaclet/) - [Proof loading / saving](ProofLoadSave/) +- [How to write new taclets](HowToTaclet/) ### SMT solver integration - [Adding an SMT solver](AddingSMTSolvers/) diff --git a/docs/quicktour/appendix.md b/docs/quicktour/appendix.md index 007d084..490f85f 100644 --- a/docs/quicktour/appendix.md +++ b/docs/quicktour/appendix.md @@ -480,7 +480,7 @@ a restricted set of signatures of classes and methods from the default standard library. The current set of classes can be found at . -For documentation on how to set up your own classpath, see [Using the classpath directives in KeY](../Classpath.md). +For documentation on how to set up your own classpath, see [Using the classpath directives in KeY](../../user/Classpath/). [^1]: Potential warnings can be safely ignored here. diff --git a/docs/user/JavaDLinJML.md b/docs/user/JavaDLinJML.md index c6c22e6..c9b0b20 100644 --- a/docs/user/JavaDLinJML.md +++ b/docs/user/JavaDLinJML.md @@ -1,7 +1,6 @@ # Embedding JavaDL expressions and functions into JML expressions *Mattias Ulbrich, 2011-08-31* - Currently, JML is the standard specification for KeY (JML★ more precisely). Though it is still possible to specify JavaDL-contracts in `.key` @@ -14,30 +13,6 @@ in the code directly. An extension of the parser provides us with this possibility now. -## DL expressions in JML - -In JML declarative specifications (i.e., anywhere but in set statements), we can -write JavaDL expressions if they are embedded into `"(* *)"`. This notation is -JML-speak for a natural-language-constraint. We use it for JavaDL expressions. - -This is helpful if syntactical concepts like binding function symbols, -new sorts, ... need to be mentioned in specifications. - -Example: -``` - -class A { - int a; - int b; - /*@ invariant (* a = javaAddInt(b, 1) *); */ - /*@ invariant a == (* javaAddInt(b, 1) *); */ - /*@ invariant a == b + 1; */ -} -``` - -All three invariants have identical meaning. - - ## Escaping JavaDL function symbol names In all JML specifications (also in set statements), function symbols known in diff --git a/docs/user/ProofSlicing/ProofSlicingShortenedChains.png b/docs/user/ProofSlicing/ProofSlicingShortenedChains.png new file mode 100644 index 0000000..84da7d2 Binary files /dev/null and b/docs/user/ProofSlicing/ProofSlicingShortenedChains.png differ diff --git a/docs/user/ProofSlicing/index.md b/docs/user/ProofSlicing/index.md index 9737099..b536576 100644 --- a/docs/user/ProofSlicing/index.md +++ b/docs/user/ProofSlicing/index.md @@ -1,6 +1,6 @@ # Proof Slicing --- *Author: Arne Keller*, December 2022 valid for KeY-2.12.0 +-- *Author: Arne Keller*, December 2022 valid for KeY-2.12.0 (last updated: November 2023) !!! abstract @@ -46,6 +46,22 @@ You may also export the dependency graph in DOT format ("Export as DOT" button) It is not advisable to render the dependency graph of large proofs: the render process may consume excessive amounts of memory and/or CPU time. +### Chain Shortening + +=== "Description" + + When inspecting the dependency graph, you might want to see only the "big picture" of the proof. + If you don't care about the hundreds of intermediate steps it takes to normalize a polynomial (for example), + you may enable the "Shorten long chains" option before rendering the graph. + When enabled, all nodes with input and output degree equal to one are collapsed into the output edge. + +=== "Example" + +
+ ![Side-by-side comparison of chain shortening](./ProofSlicingShortenedChains.png){ loading=lazy } +
Left graph: default settings. Right graph: chain shortening enabled.
+
+ ## Proof Analysis The extension offers two analysis algorithms. @@ -78,7 +94,7 @@ The "Slice proof to fixed point" button repeatedly executes the analysis and sli
Running the proof slicer creates a new proof
-## Dependency graph node types +## Dependency Graph node types All nodes store the branch location of the proof step that created them. In case of splitting proof steps, the branch of the new node is stored. @@ -99,6 +115,7 @@ Used if a proof step has no inputs / outputs to ensure that the outputs / inputs Specified as an output if the proof step creates a new skolem constant. Specified as an input if the proof steps uses the variable to instantiate a schema variable. +(Not implemented yet.) ### Taclet diff --git a/docs/user/UiFeatures/index.md b/docs/user/UiFeatures/index.md new file mode 100644 index 0000000..dcc3dc6 --- /dev/null +++ b/docs/user/UiFeatures/index.md @@ -0,0 +1,4 @@ +- [Exploration](../Exploration) +- [Node Differences](../NodeDiff) +- [Proof Slicing](../ProofSlicing) +- [Proof Caching](../ProofCaching) \ No newline at end of file diff --git a/docs/user/index.md b/docs/user/index.md deleted file mode 100644 index 81c618a..0000000 --- a/docs/user/index.md +++ /dev/null @@ -1 +0,0 @@ -# Using KeY diff --git a/mkdocs.yml b/mkdocs.yml index 7b3077e..deea199 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -82,6 +82,7 @@ theme: - navigation.indexes - navigation.top - content.code.annotate + - content.tabs.link icon: repo: fontawesome/brands/github @@ -95,7 +96,6 @@ nav: - quicktour/proving.md - quicktour/appendix.md - User Guide: - - user/index.md - changelog.md - user/FAQ.md - user/ADTs.md @@ -106,12 +106,12 @@ nav: - user/Polarity.md - user/JavaGrammar.md - UI Features: + - user/UiFeatures/index.md - user/Exploration.md - user/NodeDiff.md - user/ProofSlicing/index.md - user/ProofCaching/index.md - Languages: - - user/HowToTaclet.md - user/JMLGrammar.md - user/KeyGrammar.md - Proof Scripts: @@ -145,8 +145,9 @@ nav: - Important topics: - devel/GUIExtensions.md - devel/Listeners.md - - devel/HowtoTaclet.md - devel/ProofLoadSave.md + - devel/NewKeyParser.md + - devel/HowToTaclet.md - SMT: - devel/AddingSMTSolvers.md - devel/SMTTranslation.md diff --git a/pyproject.toml b/pyproject.toml new file mode 100644 index 0000000..e7d7081 --- /dev/null +++ b/pyproject.toml @@ -0,0 +1,24 @@ +[project] +name = "key-docs" +description = "Documentation for the KeY prover system" +readme = "README.md" +requires-python = ">=3.7" +classifiers = [ + "Operating System :: OS Independent", +] +dynamic = ["version"] +dependencies = [ + "mkdocs", + "mkdocs-material", + "pymdown-extensions", + "pygments", + "markdown-blockdiag", + "mkdocs-bibtex", + "markdown-aafigure==v202104.1011", + "mkdocs-build-plantuml-plugin", + "Pillow", + "Markdown" +] + +[tool.setuptools] +py-modules = [] \ No newline at end of file