Abstract
A structured array is an array satisfying given constraints, such as being sorted or having no duplicate values. Generation of all arrays with a given structure up to some given length has many applications, including bounded exhaustive testing. A sequential generator of structured arrays can be defined by two C functions: the first one computes an initial array, and the second one steps from one array to the next one according to some total order on the set of arrays. We formally specify with ACSL annotations that the generated arrays satisfy the prescribed structural constraints (soundness property) and that the generation is in increasing lexicographic order (progress property). We refine this specification into two programming and specification patterns: one for generation in lexicographic order and one for generation by filtering the output of another generator. We distribute a library of generators instantiating these patterns. After adding suitable loop invariants we automatically prove the soundness and progress properties with the Frama-C platform.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Arndt, J.: Matters Computational - Ideas, Algorithms, Source Code [The fxtbook] (2010). http://www.jjj.de
Baudin, P., Cuoq, P., Filliâtre, J.C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language. http://frama-c.com/acsl.html
Bobot, F., Filliâtre, J.C., Marché, C., Melquiond, G., Paskevich, A.: The Why3 platform 0.81 (March 2013). https://hal.inria.fr/hal-00822856
Bulwahn, L.: The new Quickcheck for Isabelle. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 92–108. Springer, Heidelberg (2012)
Butelle, F., Hivert, F., Mayero, M., Toumazet, F.: Formal proof of SCHUR conjugate function. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol. 6167, pp. 158–171. Springer, Heidelberg (2010)
Carlier, M., Dubois, C., Gotlieb, A.: A certified constraint solver over finite domains. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 116–131. Springer, Heidelberg (2012)
Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming. SIGPLAN Not., vol. 35, pp. 268–279. ACM, New York (2000)
Correnson, L.: Qed. computing what remains to be proved. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 215–229. Springer, Heidelberg (2014)
Dijkstra, E.W.: A Discipline of Programming. In: Series in Automatic Computation, Prentice Hall, Englewood Cliffs (1976)
Filliâtre, J.-C.: Verifying two lines of C with Why3: an exercise in program verification. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 83–97. Springer, Heidelberg (2012). http://dx.doi.org/10.1007/978-3-642-27705-4
Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Mathematical Aspects of Computer Science. Proceedings of Symposia in Applied Mathematics, vol. 19, pp. 19–32. American Mathematical Society, Providence (1967)
Gligoric, M., Gvero, T., Jagannath, V., Khurshid, S., Kuncak, V., Marinov, D.: Test generation through programming in UDITA. In: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, ICSE 2010, vol. 1, pp. 225–234. ACM, New York (2010)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)
Marinov, D., Khurshid, S.: TestEra: A novel framework for automated testing of Java programs. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering, pp. 22–31. IEEE Computer Society, Washington, DC (2001)
Paraskevopoulou, Z., Hriţcu, C.: A Coq framework for verified property based testing (2014). http://prosecco.gforge.inria.fr/personal/hritcu/publications/verified-testing-report.pdf
Petiot, G., Kosmatov, N., Giorgetti, A., Julliand, J.: How test generation helps software specification and deductive verification in Frama-C. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 204–211. Springer, Heidelberg (2014)
Ruskey, F.: Combinatorial Generation Working Version (1j-CSC 425/520) (2003). http://www.1stworks.com/ref/RuskeyCombGen.pdf
Seidel, E.L., Vazou, N., Jhala, R.: Type targeted testing. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 812–836. Springer, Heidelberg (2015)
Sullivan, K.J., Yang, J., Coppit, D., Khurshid, S., Jackson, D.: Software assurance by bounded exhaustive testing. In: Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2004, pp. 133–142. ACM (July 2004)
The OEIS Foundation Inc.: The On-Line Encyclopedia of Integer Sequences (2010). http://oeis.org
Weber, T.: SMT solvers: New oracles for the HOL theorem prover. International Journal on Software Tools for Technology Transfer 13(5), 419–429 (2011)
Williams, N.: Abstract path testing with PathCrawler. In: Proceedings of the 5th Workshop on Automation of Software Test, AST 2010, pp. 35–42. ACM, New York (2010)
Zito, A.: quickcheck4c: A QuickCheck for C (2014). https://github.com/nivox/quickcheck4c
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Genestier, R., Giorgetti, A., Petiot, G. (2015). Sequential Generation of Structured Arrays and Its Deductive Verification. In: Blanchette, J., Kosmatov, N. (eds) Tests and Proofs. TAP 2015. Lecture Notes in Computer Science(), vol 9154. Springer, Cham. https://doi.org/10.1007/978-3-319-21215-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-21215-9_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-21214-2
Online ISBN: 978-3-319-21215-9
eBook Packages: Computer ScienceComputer Science (R0)