Open Drodt opened 5 months ago
Attention: 71 lines
in your changes are missing coverage. Please review.
Comparison is base (
1fb0c10
) 37.77% compared to head (c6bc033
) 37.75%.
:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.
Intended Change
Based on #3420. Changes the JML pareser to accept definitions of ADTs. Datatypes have a list of constructors separated by
|
, and a body of functions.Currently, ADTs can only be defined on class-level, not inside methods or outside of classes.
There also is no semantics for these ADTs. KeY simply ignores them. Ideally, we want to use the defined types and functions in specification and translate them to KeY ADTs.
We also want to use the new Java switch expressions to allow pattern matching on ADTs, i.e,:
Open questions are:
l1 + l2
forl1.append(l2)
?List
class/interface?OpenJML has a similar concept of ADTs and pattern matching. For demonstration, there is a list example.
Type of pull request
Ensuring quality
Additional information and contact(s)
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.