Abstract
We present solutions to the three challenges of the VerifyThis competition held at the 18th FM symposium in August 2012. These solutions use the Why3 environment for deductive program verification.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Notes
Notice that the non-ghost fields of
can still be used in regular, non-ghost code, which would not be the case were
declared as a
type.
Another purpose of transformations is to eliminate and encode various high-level features of Why3 language, such as pattern matching or type polymorphism, to make proof obligations acceptable for a range of external provers. These transformations are invoked by a driver for a particular prover and do not need to be applied explicitly by the user.
Calling a method on an object before it is fully constructed is indeed not recommended [18].
That came to our mind during the competition.
References
Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Proceedings of the 23rd international conference on Computer aided verification, CAV’11, pp. 171–177. Heidelberg, Berlin (2011)
Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) 19th International Conference on Computer Aided Verification, vol 4590 of Lecture Notes in Computer Science, pp. 298–302. Springer, Berlin (2007)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Springer-Verlag, Berlin (2004)
Bobot, F., Conchon, S., Contejean, E., Iguernelala, M., Lescuyer, S., Mebsout, A.: The Alt-Ergo automated theorem prover. (2008) http://alt-ergo.lri.fr/
Bobot, F., Filliâtre, J.-C., Marché, C., Melquiond, G., Paskevich, A.: Preserving user proofs across specification changes. In: Cohen, E., Rybalchenko, A. (eds.) Verified software: theories, tools, experiments (5th International Conference VSTTE), vol 8164 of Lecture Notes in Computer Science, pp. 191–201. Springer, Atherton (2013)
Bobot, F., Filliâtre, J.-C., Marché, C., Melquiond, G., Paskevich, A.: The Why3 platform, version 0.82. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.82 edition. (2013) http://why3.lri.fr/download/manual-0.82.pdf
Bobot, F., Filliâtre, J.-C., Marché, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie (ed.) First International Workshop on Intermediate Verification Languages, pp. 53–64. Wrocław, Poland (2011)
de Moura, L., Bjørner, N.: Z3, an efficient SMT solver. In: TACAS, vol 4963 of Lecture Notes in Computer Science, pp. 337–340. Springer, Berlin (2008)
Filliâtre, J.-C., Paskevich, A.: Why3—where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) Proceedings of the 22nd European Symposium on Programming, vol 7792 of Lecture Notes in Computer Science, pp. 125–128. Springer, Berlin (2013)
The Frama-C platform for static analysis of C programs. (2008) http://www.frama-c.cea.fr/
Huet, G.: The Zipper. J. Fun. Progr. 7(5), 549–554 (1997)
Leino, K.R.M., Moskal, M.: VACID-0: Verification of ample correctness of invariants of data-structures. In: Proceedings of Tools and Experiments Workshop at VSTTE (2010)
Marché, C.: The Krakatoa tool for deductive verification of Java programs. Winter school on object-oriented verification, Viinistu, Estonia. (2009) http://krakatoa.lri.fr/ws/
Moy, Y., Marché, C.: The Jessie plugin for deduction verification in Frama-C – tutorial and reference manual. INRIA & LRI. (2011) http://krakatoa.lri.fr/
Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed). 11th International Conference on Automated Deduction, vol 607 of Lecture Notes in Computer Science, pp. 748–752. Springer, Saratoga Springs (1992)
Riazanov, A., Voronkov, A.: Vampire. In: Ganzinger, H. (ed.) 16th International Conference on Automated Deduction, vol 1632 of Lecture Notes in Artificial Intelligence, pp. 292–296. Springer, Trento (1999)
Schulz, S.: System description: E 0.81. In: Basin, D.A., Rusinowitch, M. (eds) Second International Joint Conference on Automated Reasoning, vol 3097 of Lecture Notes in Computer Science, pp. 223–228. Springer, Berlin (2004)
Summers, A.J., Mueller, P.: Freedom before commitment: a lightweight type system for object initialisation. In: Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications, OOPSLA ’11, pp. 1013–1032. ACM, New York (2011)
Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) 22nd International Conference on Automated Deduction, vol 5663 of Lecture Notes in Computer Science, pp 140–145. Springer, Berlin (2009)
Acknowledgments
We gratefully thank the editors and the anonymous referees for providing us very valuable comments and suggestions to improve the quality of this paper.
Author information
Authors and Affiliations
Corresponding author
Additional information
Work partly supported by the Bware project of the French national research organization (ANR-12-INSE-0010, http://bware.lri.fr/).
Appendix: Relevant theories from the Why3 standard library
Appendix: Relevant theories from the Why3 standard library
In this Appendix, we provide details on relevant parts of the Why3 standard library, notably those used in the first challenge. The full contents of that library is available online at http://why3.lri.fr/stdlib-0.81/.
Theory of polymorphic, purely applicative maps
1.1 A.1 Library map
In Why3, arrays are modeled as references to purely applicative maps. Such maps are specified in the theory presented in Fig. 22. These maps are parametric in both the type of their indexes and of their values, so the Why3 type for such maps is a polymorphic type
. The main functions operating on maps are
and
, that, respectively, modify a map at a given index (purely applicatively, that is by returning a new map) and read a map at a given index. Both functions are axiomatized by
and
. This is the classical theory of arrays in the context of satisfiability modulo theories. The additional operation
returns a constant map.
Theory of sorted maps
Theory of map permutations (excerpt)
Theory of injective and surjective maps
Theory (Fig. 23) specifies what it means for a map to be sorted in increasing order. This notion is restricted to maps indexed by integers. The theory is written with a type parameter
and a predicate parameter
, so that it can be reused, by cloning it, for an arbitrary order relation.
Module (excerpt)
Theory (Fig. 24) specifies what it means for two maps to be permutations of each other, that is, to contain the same elements with the same number of occurrences. This is restricted to maps indexed by integers. Predicate (
\(m_1\, m_2\, l\, u\)) holds when map segments \(m_1[l\ldots u-1]\) and \(m_2[l\ldots u-1]\) are permutations of each other. This is defined as the smallest equivalence relation containing transpositions of elements.
Theory (Fig. 25) defines several notions for maps on the domain \(0\ldots n-1\) for some integer \(n\): being injective, being a surjection into \(0\ldots n-1\), and ranging into \(0\ldots n-1\). Lemma
is the classical mathematical result, more or less equivalent to the pigeon-hole principle, saying that any injection that ranges into \(0\ldots n-1\) is also surjective. This result is used to prove the first challenge. This is not the first time we had to use such a result to prove a program: we already used it to prove the challenge Sparse Arrays from the VACID-0 benchmarks [12].
1.2 A.2 Module Array
Figure 26 contains an excerpt of the Why3 module that defines arrays. This module is discussed in Sect. 2.2. The full contents of that library is available online at http://why3.lri.fr/stdlib-0.81/array.mlw.html.
Rights and permissions
About this article
Cite this article
Bobot, F., Filliâtre, JC., Marché, C. et al. Let’s verify this with Why3. Int J Softw Tools Technol Transfer 17, 709–727 (2015). https://doi.org/10.1007/s10009-014-0314-5
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-014-0314-5