David R. Cok
ABSTRACT
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.
- P. Baudin, P.Cuoq, J-C. Filliâtre, C. Marché, B. Monate, Y. Moy, and V. Prevosto. 2008ff. ACSL: ANSI C Specification Language. http://frama-c.com/download/acsl_1.4.pdf.Google Scholar
- David R. Cok and Serdar Tasiran. 2018. Practical Methods for Reasoning about Java 8's Functional Programming Features. Submitted to VSTTE 2018.Google Scholar
- Frama-C 2011ff. https://frama-c.com.Google Scholar
- Bart Jacobs, Jan Smans, and Frank Piessen. 2017. The VeriFast Program Verifier: A Tutorial. https://zenodo.org/record/1068185#.WvbWhy97HyU.Google Scholar
- I. T. Kassios and P. Müller. 2011. Modular Specification and Verification of Delegation with SMT Solvers. Technical Report. ETH Zurich.Google Scholar
- Matthew Parkinson and Gavin Bierman. 2005. Separation Logic and Abstraction. In Proceedings of the 32Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '05). ACM, New York, NY, USA, 247--258. Google ScholarDigital Library
- VESSEDIA. 2018. The work on C++ specification is part of the VESSEDIA project https://vessedia.eu. The VESSEDIA project has received funding from the European Union's Horizon 2020 research and innovation programme under grant agreement No. 731453.Google Scholar
- Reasoning about functional programming in Java and C++
Recommendations
Specifying java iterators with JML and Esc/Java2
SAVCBS '06: Proceedings of the 2006 conference on Specification and verification of component-based systemsThe 2006 SAVCBS Workshop has posed a Challenge Problem on the topic of specifying iterators. This note provides a specification in the Java Modeling Language (JML) [1, 2] for the Java interfaces Iterator and Iterable that captures the interactions ...
OpenJML: JML for Java 7 by extending OpenJDK
NFM'11: Proceedings of the Third international conference on NASA Formal methodsThe Java Modeling Language is a widely used specification language for Java. However, the tool support has not kept pace with advances in the Java language. This paper describes OpenJML, an implementation of JML tools built by extending the OpenJDK Java ...
Functional programming, formal specification, and rapid prototyping
Functional programming has enormous potential for reducing the high cost of software development. Because of the simple mathematical basis of functional programming it is easier to design correct programs in a purely functional style than in a ...
Comments