key

key copied to clipboard

Introduce JML aliases of frame conditions for better tool compatibility

9

This pull request allows handling various aliases for frame conditions within method/block/loop contracts and loop specifications. These aliases cover the ones which are used in various other verification tools with...

mi-ki

Generalize ParsableVariable and Schemavariables

1

## Related Issue ## Intended Change This PR moves the `ParsableVariable` interface to `ncore`, makes it no longer an `Operator` and renames `AbstractSV` to `OperatorSV` as this interface now handles...

Drodt

Hackeython unknown methods

1

## Related Issue This pull request addresses #1663 ## Intended Change When using a library method without an explicit contract, instead of getting stuck in the proof, KeY now assumes...

flo2702

Renovation of the TestCase generation

1

## Intended Change Make test case generation usable again, especially, from the CLI in the new verification template. ## Type of pull request - *X* Refactoring (behaviour should not change...

wadoon

Nullness Type System for `key.core`

2

More nullness type system checks. Now for `key.core`. I want first to merge #3399 into KeY to avoid double work.

wadoon

The Removal of Recoder

83

This PR replaces recoder by [javaparser](https://github.com/javaparser/javaparser), or more precisely by [key-javaparser](https://github.com/wadoon/key-javaparser). The special version has support for `ProofJava`, `SchemaJava` and Java 17+, all in one grammar. [Notes on the grammar...

wadoon

Allow realizing multiple cached branches at once

2

## Intended Change This PR changes the "Copy referenced proof steps here" action to allow applying it on any node that has leaf children with caching info. It will then...

FliegendeWurst

Create a JSON-RPC for KeY

3

# A remote KeY api as promised in KeY++ ## Design Descisions * We use handles to refer to large entities like, `KeYEnvironment`, `Proof`, or `Node`. These handles are called...

wadoon

This PR removes the remaining traces of JUnit 4 completely from KeY. JUnit 5 offers the same functionalities in a simpler matter, therefore there is no need to keep JUnit...

wadoon

Revive work on Polymorphic Sorts

2

Introducing Sorts with Sort-Parameters. ## Type of pull request - *X* New feature (non-breaking change which adds functionality) - *X* Breaking change (fix or feature that would cause existing functionality...

wadoon