Reasoning about Functional Programming in Java and C++.

Verification projects on industrial code have required reasoning about functional programming constructs in Java 8. General functional programming requires reasoning about how the specifications of function objects that are inputs to a method combine to produce the specifications of output function objects. This short paper describes our in-progress experience in adapting prior work (Kassios & Müller) to Java 8, JML, OpenJML, and to ACSL++, a specification language for C++ built on ACSL.