Lambda Expressions

[wadoon]

Currently, jmlparser misses support of lambda expression. I think we should start to settle definitions for lambda expressions and higher order functions. I see the following the discussion points:

1. How to specify a lambda expression? For example:

   var fn1 = /*@ ..contract..*/ (a,b) -> { return a + b; }
   var fn2 = (a,b) -> /*@ ..contract.. */ { return a + b; }

   • Where should the JML contract placed?
   • Is it a normal method contract or should we allow or forbid certain clauses/behaviors?
   • How to deal with assignments:

     MySingleAbstractInterface fn2 = (a,b) -> /*@ ..contract.. */ { return a + b; }

     The inline contract has to be sub-contract of the every contract at the SAM in the interface.

2. How to use higher order functions (lambda expression or method references) inside JML constructs? Beside the use inside contracts or invariants, we also have the ghost statements which could enclose local variables.

   • I think we mainly need to define when a lambda expression is pure.

3. How to specify requirements on a given higher order function? Image you have a function like:

   /*@ assignable \nothing; */
   public int foo(Supplier<Integer> fn) { return fn.get(); }

   How can I specify that the given Supplier also has assignable \nothing; clause?

   • Do we need to contracts accessible from JML?

     //@ requires \contract_of(fn).assignable == \nothing;

Do I missed a discussion point?

Support for lambda expression in KeY were explored by @mattulbrich and @csicar.

[mattulbrich]

I think it is a really interesting topic, but I wonder if it can really be covered in a github issue ;-P

Carsten has written his thesis on how to deal with that in KeY using a variety of options, and David has an experience report on dealing with lambdas in practice.

[wadoon]

I think it is a really interesting topic, but I wonder if it can really be covered in a github issue ;-P

The alternative would be a call or a JML workshop :)

I hope, we can at least collect the discussion points, and then proceed the substantial discussion.

[davidcok]

This is a significant topic. It is not sufficient just to have syntactical/language design ideas. They need to be worked out in the context of actual verification problems and the common usage of lambda expressions.

There is another alternative to the syntax Remember that in Java all lambda functions are instances of a functional interface. One cannot have a stand-alone lambda expression. It is always in a context in which its type can be inferred. That means we can use specification-level type casting to give a type with specifications.

For example, Java has a Function<T,U>, whose specification is so general it cannot be used to prove anything. But we can write

@FunctionalInterface
interface PurePredicate<T> extends Predicate<T> {

  //@ also public normal_behavior
  //@   assigns \nothing;
  boolean test(T t);
}

and then in actual use

public static boolean all(List<Integer> list, Predicate<Integer> predicate) {
  return list.stream().allMatch(i -> (/*@ (PurePredicate<Integer>)*/predicate).test(i));
}

or even just

public static boolean all(List<Integer> list, Predicate<Integer> predicate) {
  return list.stream().allMatch(/*@ (PurePredicate<Integer>)*/predicate);
}

Of course, there is a proof obligation that the predicate being cast actually conforms to the more restricted specification. So one might want some syntax for the signature as well:

public static boolean all(List<Integer> list, /*@{PurePredicate<Integer>}*/ Predicate<Integer> predicate) {
  return list.stream().allMatch(i -> predicate.test(i));
}

to indicate that, for specification purposes, the argument has a more restricted type -- and then when all is called, say with all(list, k->k>0), one must prove that the given lambda function satisfies the spec of PurePredicate, not just Predicate.

If you have control fo the source code, you can just use PurePredicate where you like. But the library methods for functions and streams use classes with very general specs that cannot be reasoned with.

I find that naming a specification with an interface declaration a) is more readable -- name shows intent and oe can see where the same spec is reused b) allows reuse of the specification, simplifying proof obligations c) fits existing Java syntax more closely with the one downside of d) the actual specs are in a place different than where used (in the same way that a called methods specs are placed with the method declaration rather than its point of use)

[leavens]

I agree that this is a research topic that deserves further treatment.