Published: 26th April 2014
DOI: 10.4204/EPTCS.149
ISSN: 2075-2180

EPTCS 149

Proceedings 1st Workshop on
Formal Integrated Development Environment
Grenoble, France, April 6, 2014

Edited by: Catherine Dubois, Dimitra Giannakopoulou and Dominique Méry

Preface
The Gotthard Approach: Designing an Integrated Verification Environment for Eiffel
Carlo A. Furia, Julian Tschannen and Bertrand Meyer
1
The Dafny Integrated Development Environment
K. Rustan M. Leino and Valentin Wüstholz
3
Who watches the watchers: Validating the ProB Validation Tool
Jens Bendisposto, Sebastian Krings and Michael Leuschel
16
Teaching Formal Methods and Discrete Mathematics
Mathieu Jaume and Théo Laurent
30
SPEEDY: An Eclipse-based IDE for invariant inference
David R. Cok and Scott C. Johnson
44
Experience in using a typed functional language for the development of a security application
Damien Doligez, Christèle Faure, Thérèse Hardin and Manuel Maarek
58
FoCaLiZe: Inside an F-IDE
François Pessaux
64
OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse
David R. Cok
79
Checking Computations of Formal Method Tools - A Secondary Toolchain for ProB
John Witulski and Michael Leuschel
93

Preface

High levels of safety, security and also privacy standards require the use of formal methods to specify and develop compliant software (sub)systems. Any standard comes with an assessment process, which requires a complete documentation of the application in order to ease the justification of design choices, code review and proofs. F-IDE (Formal Integrated Development Environment) is dedicated to such developments that should comply with several requirements. The first one is to associate a logical theory with a programming language, in a way that facilitates the tightly coupled handling of specification properties and program constructs. The second one is to offer a language/environment simple enough to be usable by most developers, even if they are not fully acquainted with higher-order logics or set theory, in particular by making development of proofs as easy as possible and as readable as possible. The third one is to offer automated management of application documentation. It may also be expected that developments done with such an F-IDE are reusable and modular. Moreover, tools for testing and static analysis may be embedded in this F-IDE, to address most steps of the assessment process.

The workshop F-IDE is the first one on those topics and welcomed submissions in the following areas, among others:

We encouraged not only mature research results but also submissions presenting innovative ideas and early results are also of interest. Eight communications are compiled in this volume and were presented during the one day meeting (April 6, 2014) in Grenoble.

In this volume, a communication is presenting OpenJML; it is a tool for software verification of Java programs in the contract-based approach and demonstrates the value of integrating specification and verification tools directly in the software development IDE and in automating as many tasks as possible. Two other communications describe Integrated Development Environments like for Dafny or as SPEEDY and show how these tools are useful in practical cases. Several communications concern FoCaliZe and illustrate the reply of this environment for meaning what is a formal IDE. Another communication reports on the use of a typed functional language for developing a secure application. Finally, two communications focus on the validations efforts for the validation tool ProB, in a quest of certification, e.g. in the context of the EN50128 norm and safety critical applications in the railway domain.

The program committee of F-IDE 2014 was composed of:

Bernhard Beckert, Karlsruhe Institute of Technology, Germany
Loïc Correnson, CEA, France
Catherine Dubois, ENSIIE, France
Dimitra Giannakopoulou, NASA, USA
Thérèse Hardin, University Pierre and Marie Curie, France
Peter Lammich, Technische Universität München, Germany
Rustan Leino, Microsoft Research, USA
Michael Leuschel, University of Düsseldorf, Germany
Claude Marché, INRIA, France
Dominique Méry, University of Nancy, France
Suzette Person, NASA, USA
François Pessaux, ENSTA ParisTech, France
Marie-Laure Potet, ENSIMAG, France
Mike Whalem, University of Minnesota Software Engineering Center, USA

We thank the program committee members who studied very carefully the submitted papers and helped with their valuable comments to prepare this workshop. We thank Thérèse Hardin who contributed to the initiation of the event and François Pessaux who designed and maintained the F-IDE website. We are very grateful to the ETAPS organizers for taking care of all the local organization.


The Gotthard Approach: Designing an Integrated Verification Environment for Eiffel

Carlo A. Furia (Chair of Software Engineering, Department of Computer Science, ETH Zurich, Switzerland)
Julian Tschannen (Chair of Software Engineering, Department of Computer Science, ETH Zurich, Switzerland)
Bertrand Meyer (Chair of Software Engineering, Department of Computer Science, ETH Zurich, Switzerland)

We use the construction of the Gotthard tunnel – connecting the German- and Italian-speaking parts of Switzerland through the Gotthard massif – as a metaphor for the two-pronged design of the Eiffel Verification Environment (EVE). No prior knowledge of Swiss geography is required to enjoy the presentation.

Like a tunnel that connects people speaking two different languages, EVE tries to cater to two different kinds of users. At one end are the Joes Six-Pack of verification: run-of-the-mill programmers with little or no background in formal methods, who are used to standard integrated development environments but cannot be expected to write or understand complex formal specifications. At the other end are highly-trained experts, fluent in formal techniques, to whom writing and reasoning about rigorous specifications is second nature. The design of EVE accommodates features useful at both ends.

For programmers unacquainted with verification, EVE supports lightweight techniques which work with the simple contracts that most Eiffel programmers can write [2]:

For full-fledged verification experts, EVE integrates AutoProof [10], an auto-active [3] advanced program verifier which supports a large part of the Eiffel language. AutoProof's input language also features support for annotations availing of mathematical models and other specification idioms such as quantifiers and ghost code. AutoProof's logic is based on a flexible “semantic” methodology [8] to specify and reason about invariants of both hierarchical and collaborative object structures; this enables the full verification of complex design patterns, such as Observers and Composites [9], with reasonable annotation burden. The AutoInfer framework [12] is another component of EVE geared to strong specifications: it automatically infers postconditions of routines, often achieving high percentages of correctness and completeness.

The introduction of new features and the improvement of existing ones continues at both ends of the formality spectrum. Integration also progresses through EVE's architecture, which allows the various tools to run in parallel, collects their results, and displays them within a simple uniform interface that indicates, for each element such as routine or class, how much its verification has progressed, and what actions could be undertaken to improve the quality of the program under development.

The ultimate goal of EVE's ongoing double-ended development is meeting in the middle: once the tunnel is completed, it will provide a way to smoothly transition into formal techniques from everyday's programming practices.

References

  1. Ilinca Ciupa, Alexander Pretschner, Manuel Oriol, Andreas Leitner & Bertrand Meyer (2011): On the number and nature of faults found by random testing. Softw. Test., Verif. Reliab. 21(1), pp. 3–28, doi:10.1002/stvr.415.
  2. H.-Christian Estler, Carlo A. Furia, Martin Nordio, Marco Piccioni & Bertrand Meyer (2014): Contracts in Practice. In: Proceedings of the 19th International Symposium on Formal Methods (FM), Lecture Notes in Computer Science 8442. Springer.
  3. K. Rustan M. Leino & MichałMoskal (2010): Usable Auto-Active Verification. In: Usable Verification Workshop. http://fm.csl.sri.com/UV10/.
  4. Bertrand Meyer, Arno Fiva, Ilinca Ciupa, Andreas Leitner, Yi Wei & Emmanuel Stapf (2009): Programs That Test Themselves. IEEE Computer 42(9), pp. 46–55, doi:10.1109/MC.2009.296.
  5. Yu Pei, Carlo A. Furia, Martin Nordio & Bertrand Meyer (2014): Automatic Program Repair by Fixing Contracts. In: Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE), Lecture Notes in Computer Science 8411. Springer, pp. 246–260, doi:10.1007/978-3-642-54804-8_17.
  6. Yu Pei, Carlo A. Furia, Martin Nordio, Yi Wei, Bertrand Meyer & Andreas Zeller (2014): Automated Fixing of Programs with Contracts. IEEE Transactions on Software Engineering PP(99), doi:10.1109/TSE.2014.2312918.
  7. Yu Pei, Yi Wei, Carlo A. Furia, Martin Nordio & Bertrand Meyer (2011): Code-Based Automated Program Fixing. In: Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE'11). ACM, pp. 392–395, doi:10.1109/ASE.2011.6100080.
  8. Nadia Polikarpova, Julian Tschannen, Carlo A. Furia & Bertrand Meyer (2014): Flexible Invariants Through Semantic Collaboration. In: Proceedings of the 19th International Symposium on Formal Methods (FM), Lecture Notes in Computer Science 8442. Springer.
  9. (2001–2010): SAVCBS Workshop Series. http://www.eecs.ucf.edu/~leavens/SAVCBS/.
  10. Julian Tschannen, Carlo A. Furia, Martin Nordio & Bertrand Meyer (2012): Automatic Verification of Advanced Object-Oriented Features: The AutoProof Approach. In: Tools for Practical Software Verification – LASER 2011, International Summer School, Lecture Notes in Computer Science 7682. Springer, pp. 133–155, doi:10.1007/978-3-642-35746-6_5.
  11. Julian Tschannen, Carlo A. Furia, Martin Nordio & Bertrand Meyer (2014): Program Checking With Less Hassle. In: Proceedings of the 5th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE 2013), Lecture Notes in Computer Science 8164. Springer, pp. 149–169, doi:10.1007/978-3-642-54108-7_8.
  12. Yi Wei, Carlo A. Furia, Nikolay Kazmin & Bertrand Meyer (2011): Inferring Better Contracts. In: Proceedings of the 33rd International Conference on Software Engineering (ICSE). ACM, pp. 191–200, doi:10.1145/1985793.1985820.
  13. Yi Wei, Yu Pei, Carlo A. Furia, Lucas S. Silva, Stefan Buchholz, Bertrand Meyer & Andreas Zeller (2010): Automated Fixing of Programs with Contracts. In: Proceedings of the 19th International Symposium on Software Testing and Analysis (ISSTA). ACM, pp. 61–72, doi:10.1145/1831708.1831716.