Support for JML`\TYPE` - Githubissues

KeYProject / key

KeY Theorem Prover for Deductive Java Verification

https://key-project.org

Other

44 stars 24 forks source link

Support for JML`\TYPE` #3465

Closed flo2702 closed 5 months ago

flo2702 commented 5 months ago

Related Issue

This pull request addresses #3407.

Intended Change

KeY now supports the type \TYPE, the subtype operator <:, and the function \type.

The following method contract illustrates their semantics:

class A {

    int f;

    //@ ghost \TYPE packed;
    //@ invariant packed <: \type(A) ==> f > 0;
}

class B extends A {
    //@ invariant packed <: \type(B) ==> f > 1;

    //@ requires this.packed == \type(B);
    //@ ensures f > 0;
    //@ ensures f > 1;
    void subtypes() {}
}

Type of pull request

New feature (non-breaking change which adds functionality)
There are changes to the (Java) code
There are changes to the taclet rule base

Ensuring quality

I made sure that introduced/changed code is well documented (javadoc and inline comments).
I added new test case(s) for new functionality.
I have checked that runtime performance has not deteriorated.

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.