Hackeython: ADTs in JML

[Drodt]

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.

class Test {
	/*@ datatype List {
	  @ 	Nil()
	  @	| Cons(\any head, List tail);
	  @
	  @ 	int size() {
	  @		return 0;
	  @ 	}
	  @ }
	  @*/
}

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,:

switch (list) {
  case Nil -> 0;
  case Cons(_, xs) -> 1 + xs.size();
}

Open questions are:

• How are JML ADTs translated to KeY?
• How are switch expressions with pattern matching translated?
• Can we define a shorthand infix notation for ADT function, e.g., l1 + l2 for l1.append(l2)?
• How do we resolve ADT function calls in specification?
• What happens if we already have a List class/interface?

OpenJML has a similar concept of ADTs and pattern matching. For demonstration, there is a list example.

Type of pull request

• Bug fix (non-breaking change which fixes an issue)
• Refactoring (behaviour should not change or only minimally change)
• New feature (non-breaking change which adds functionality)
• Breaking change (fix or feature that would cause existing functionality to change)
• There are changes to the (Java) code
• There are changes to the taclet rule base
• There are changes to the deployment/CI infrastructure (gradle, github, ...)
• Other: Changes to ANLTR grammars

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
• I added new test case(s) for new functionality.
• I have tested the feature as follows: ...
• I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

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

[codecov]

Codecov Report

Attention: 71 lines in your changes are missing coverage. Please review.

Comparison is base (1fb0c10) 37.77% compared to head (c6bc033) 37.75%.

Files	Patch %	Lines
...e/uka/ilkd/key/nparser/builder/TacletPBuilder.java	0.00%	56 Missing ⚠️
.../key/nparser/builder/FunctionPredicateBuilder.java	0.00%	14 Missing ⚠️
...a/ilkd/key/nparser/builder/DeclarationBuilder.java	0.00%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3427      +/-   ##
============================================
- Coverage     37.77%   37.75%   -0.03%     
+ Complexity    17031    17030       -1     
============================================
  Files          2076     2076              
  Lines        126950   127017      +67     
  Branches      21381    21388       +7     
============================================
- Hits          47952    47951       -1     
- Misses        73092    73159      +67     
- Partials       5906     5907       +1     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[wadoon]

One of the primary todos might be to prepare a proposal for JMLref.

[mattulbrich]

OpenJML used "," where Daniel @Drodt proposed "|". Small detail. I think in the face of enums, "," would fit better into the Java biotope.

[mattulbrich]

I just had a look at the axioms created for ADTs. There seems to be an unexpected "not free in" condition.
Perhaps we can review this, too, while we are working on it during the hackeython.

Color_Axiom {
  \schemaVar \formula phi;
  \schemaVar \variables Color x;
  
  \find(\forall x; phi)
  \varcond(\notFreeIn(x, phi))
  \add(
         \forall x; phi
     <->   {\subst x;Red}phi
         & {\subst x;Green}phi
         & {\subst x;Blue}phi
    ==>
  )
  \displayname "Axiom_for_Color"
}

[mattulbrich]

Discussion at the HackKeYthon:

• free generated: important, but what about not-free variants (like finite sets, maps)
• switch with pattern matching as generalisation of if in KeY JavaDL.
• Termination witness proofs not needed for subterms of termination witness inputs (at least when using pattern matching)
• Syntax and Java-similarity: Merge the intuition of enum and record.
• Selectors are important
• Parametric polymorphism is important

@TudorBalan

[Drodt]

Thanks!

Discussion at the HackKeYthon:

* free generated: important, but what about not-free variants (like finite sets, maps)

Can you elaborate what you mean by free here?

* `switch` with pattern matching as generalisation of `if` in KeY JavaDL.

* Termination witness proofs not needed for subterms of termination witness inputs (at least when using pattern matching)

What are the issues when not pattern matching?

* Syntax and Java-similarity: Merge the intuition of enum and record.

What intuition? How do you plan to merge?

* Selectors are important

In what way? Which selectors?

* Parametric polymorphism is important

Any progress on that front? Did you consider the more type class oriented approach or is that too dissimilar to Java?

[philipppk]

After implementing switch expressions into the parser for key files, we discussed how it should be represented as a term in key and the semantics of a switch expression

switch expressions as a term

We propose to add the terms

term	sort	argumentsorts
U,T::switch	T	U, U,T::case
U,T::case	U,T::case	U, T, U,T::case
U,T::default	U,T::case	T
U,T::nodefault	U,T::case

Adding the case term is necessary so switch can have arbitrarily many cases. Default cases stating a catch all value and no default cases can be used to close a cascade of cases.

switch semantics

Instead of giving the semantics of the newly introduced terms we give the semantics of an example switch statement (I also upload the discussion from the whiteboard so nothing is lost)

The expression

switch (exp) (
   case (C1) -> T1
   case (C2(x)) -> T2(x)
   default -> T3
)

should evaluate to

$$\epsilon x.((exp=C1->x=T1)\wedge \mathrm{\forall }y.(exp=C2(y)->x=T2(y))\wedge exp\ne C1\wedge \mathrm{\forall }y.(exp\ne T2(y))\to x=T3)$$

Here @mattulbrich proposed to use the Hilbert $\epsilon$ operator, which has the meaning that x is an underspecified value for which the statements that follow after are true.

[mattulbrich]

Discussion at the HackKeYthon:
free generated: important, but what about not-free variants (like finite sets, maps)

Can you elaborate what you mean by free here?

Free here means that different ground terms denote different semantic values. Like a language with concatenation the free monoid on the alphabet (words are equal only if the same sequence of letters. Lists in this sense are free (wrt. to their constrcutors) while finite sets are not ({1,2} being the same as {2,1}) (wrt to insert and empty).

Termination witness proofs not needed for subterms of termination witness inputs (at least when using pattern matching)

What are the issues when not pattern matching?

In the example of a list: Calling a.tail() is not necessarily decreasing because a can be nil. But if a variable is bound within a pattern matching, then it is syntactically clear that this variable is smaller in the sub-adt sense. Otherwise it comes with some semantic conditions (like a != nil for a.tail()).

Syntax and Java-similarity: Merge the intuition of enum and record.
Enum: List the different possibilities of values as elements in the type body
Records: List the named values with types as arguments to the constructors.
In both cases: Allow further operations after ";".

What intuition? How do you plan to merge?

The similarity with enums would obviously lead to a comma as separator between constructors. 😛
But pipe is fine, too, I guess.
Actually, Daniel @Drodt 's proposal has this already implemented. Is rather obvious. So does David Cok's in OpenJML.

Selectors are important

Selectors = Destructors

Parametric polymorphism is important

Any progress on that front? Did you consider the more type class oriented approach or is that too dissimilar to Java?

See elsewhere ...

[mattulbrich]

Another important observation is the following:

In order to avoid name clashes, constructors need to be prefixed with the type. I.e. for

package pack.path;
datatype List { Nil | Cons(int value, List list) }

one needs to write pack.pah.List.Nil to refer to nil to avoid name clashes.
As usual with Java, one can use import to be allowed to shorten this like:

import static pack.path.List.*;

Now Nil suffices ... In KeY, probably the full name should be used ...

[mattulbrich]

After implementing switch expressions into the parser for key files, we discussed how it should be represented as a term in key and the semantics of a switch expression

Thanks, @philipppk! A few more explaining words:

When translating such switch-case JML expressions into JavaDL, we can use existing infrastructure or use new infrastructure. Using the Hilbert-Epsilon operator is nice because it reuses existing structures. However, during normalisation the structure of the argument of the operator may be modified such that specialised taclet or pretty printing may no longer apply. And the epsilon-presentation is not exactly user-friendly.

When using a specialised JavaDL syntax with new constructors (cases, nodefault, default, switch), normalisation cannot destroy the structure of expression, yet we need many new rules to deal with the situation.

At any rate:

"if" should/could be retrofitted as a special case of switch case.
"ifEx" has a certain similarity with the case function above, also regarding polymorphic properties....

[mattulbrich]

I would like to to tell David Cok from openjml about these advances and would like to mention that syntax-wise the languages are compatible. This would mean that we could perhaps support both | and , as separators between constructors for compatibility reasons.
OK?

[mattulbrich]

Followup in next KeY meeting: We could introduce a switch operator per term with the appropriate signature thus avoiding a vari-arity symbol.

[mattulbrich]

Followup in next KeY meeting: We could introduce a switch operator per term with the appropriate signature thus avoiding a vari-arity symbol.

Actually, it turns out that this can be generally implemented into KeY generally w/o touch a single line of Java code.

The example switch.key (pls remove the file extension .txt) shows how a new function symbol switchList can be introduced realising switch expressions for the List adt. It takes three arguments: switchList(term, nilCase, consCase) with the nilCase a constant value and the consCase a "double abstraction", i.e. a term of the form "λhead. λtail. term_using(head, tail)".

Those are not part of KeY at the moment, so I added a new type binding (whose intuition is any→any) with a constructor bind (whose intuition is λ abstraction) and an observer G::apply (whose intuition is function application of λ-calculus).
There is the obvious ß-reduction axiom that defines the setup.

Since KeY does not support parameterised types, it is all a bit ugly regarding the typing, but still sound.

[wadoon]

I started with the JML implementation part.
There are some questions about ADT in the real-world/key-world.

• How to deal with mutual definition of ADT in JML? Note JML comments are merged and a block is processed at the same time.
• Are ADTs living in fully-qualified namespaces?
• Does ADTs need to be imported? (e.g., //@ import model my.adt.List;)
• Inner ADTs are allowed?
• ...

[wadoon]

Short floor discussion:

• ADTs should be fully-qualified
• ADTs should also be possible on Type-declaration-level (directly in compilation units)
• model-import should be possible (but hard to implement in recoder)

[wadoon]

@mattulbrich @WolframPfeifer

Just a quick thought: Why do we invent our own ADT stuff when there are established tools for functional verification? Would it not be funny to have something like "functional Java" (which is obviously F*/Haskell with Java-style Syntax)? (Or do we have reached this point with allowing more stuff in model methods?)

[mattulbrich]

Just a quick thought: Why do we invent our own ADT stuff when there are established tools for functional verification? Would it not be funny to have something like "functional Java" (which is obviously F*/Haskell with Java-style Syntax)? (Or do we have reached this point with allowing more stuff in model methods?)

That is indeed the idea of switch expressions, model methods and ADT declarations. ...