fixes #3670: KeY does not know that enum constants are non-null

[mattulbrich]

Related Issue

This pull request resolves #3670.

Intended Change

Enum constants are finally supported again (after initial support between 2006 and 2011).

Features

• Constants are unique
• Constants are never null
• their value of .ordinal() can be retrieved.

Type of pull request

• New feature (non-breaking change which adds functionality): Bringing back functionality that was once there.
• There are changes to the (Java) code: rather locally in some varcond and meta function classes.
• There are changes to the taclet rule base: java5.key has been touched

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments). yes
• I have tested the feature as follows: ...

I would like to leave this to @FliegendeWurst and @WolframPfeifer who need this feature in a case study and can study this there, find bugs and add test cases from the study.

Additional information and contact(s)

Case study by @FliegendeWurst, @WolframPfeifer

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

[mattulbrich]

I tested it on this code. The methods can be verified. Alas, different has an open branch because Severity.INFO must be proven to be created. Perhaps a rule similar to the other new rules can be added.

public enum Severity {
    INFO,
    WARNING,
    CRITIQUE	
}

public class Checker {
    /*@ public normal_behaviour
      @ ensures \result != null;
      @*/
    Severity checkIt() {
        return Severity.INFO;
    }

    /*@ public normal_behaviour
      @  ensures \result == 1;
      @*/
    int ord() {
        return Severity.WARNING.ordinal();
    }

    /*@ public normal_behaviour
      @  ensures \result != Severity.CRITIQUE;
      @*/
    Severity different() {
        return Severity.INFO;
    }
}

[mattulbrich]

Please check for logical soundness. It felt correct, but I have not really checked.

[wadoon]

As far as I would tell is that the support is incomplete:

1. Is e <: java.lang.Enum valid for all enums instances e?
2. Some methods are missing of java.lang.Enum
3. The static generated E.values() method is missing.

Do you think, we should rather downcompile to Java with final fields?

[wadoon]

It seems that this class is inside the immutable KeY Java AST.

Can we avoid a mutable data structure here?

I would say that an ImmutableList<IProgramVariables> should be enough.

[mattulbrich]

An immutable map would work. It has been a mutable DS before.

[FliegendeWurst]

This breaks if the enum constructor throws an exception.

JMERuleErrorSeverity.java

public enum JMERuleErrorSeverity {
    INFO,
    WARNING,
    CRITIQUE;
    
    JMERuleErrorSeverity() {
        throw new IllegalStateException();
    }
}

Main.java

public class Main {
	public static void main(String[] args) {
		System.out.println(JMERuleErrorSeverity.INFO);
	}
}

[wadoon]

In which sense, does this break for errors during initialization?

The JLS gives no direct answer. The nearest case would be "Example 8.9.2-1. Restriction On Enum Constant Self-Reference".