Abstract
Specifications are key to improving software reliability as well as documenting precisely the intended behavior of software. Writing specifications is still perceived as expensive. Of course, writing implementations is at least as expensive, but is hardly questioned because there is currently no real alternative. Our goal is to give specifications a more balanced role compared to implementations, enabling the developers to compile, execute, optimize, and verify against each other mixed code fragments containing both specifications and implementations. To make specification constructs executable we combine deductive synthesis with run-time constraint solving, in both cases leveraging modern SMT solvers. Our tool decomposes specifications into simpler fragments using a cost-driven deductive synthesis framework. It compiles as many fragments as possible into conventional functional code; it executes the remaining fragments by invoking our constraint solver that extends an SMT solver to handle recursive functions. Using this approach we were able to execute constraints that describe the desired properties of integers, sets, maps and algebraic data types.
This work is supported in part by the European Research Council (ERC) Project Implicit Programming.
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
Ait-Kaci, H.: Warren’s Abstract Machine: A Tutorial Reconstruction. MIT Press (1991)
Antoy, S.: Definitional trees. In: ALP, pp. 143–157 (1992)
Antoy, S., Hanus, M.: Functional logic programming. CACM 53(4), 74–85 (2010)
Asarin, E., Maler, O., Pnueli, A.: Symbolic controller synthesis for discrete and timed systems. In: Hybrid Systems II, pp. 1–20 (1995)
Back, R.-J., von Wright, J.: In: Refinement Calculus, Springer (1998)
Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006)
Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers 58 (2003)
Bierman, G.M., Gordon, A.D., Hritcu, C., Langworthy, D.E.: Semantic subtyping with an SMT solver. In: ICFP, pp. 105–116 (2010)
Blanc, R.W., Kneuss, E., Kuncak, V., Suter, P.: An overview of the Leon verification system: Verification by translation to recursive functions. In: Scala Workshop (2013)
Bodden, E., Lam, P., Hendren, L.J.: Partially evaluating finite-state runtime monitors ahead of time. ACM Trans. Program. Lang. Syst. 34(2), 7 (2012)
Braßel, B., Hanus, M., Müller, M.: High-level database programming in Curry. In: Hudak, P., Warren, D.S. (eds.) PADL 2008. LNCS, vol. 4902, pp. 316–332. Springer, Heidelberg (2008)
Bruynooghe, M., Schreye, D.D., Krekels, B.: Compiling control. The Journal of Logic Programming 6(12), 135–162 (1989)
Butler, M., Grundy, J., Langbacka, T., Ruksenas, R., von Wright, J.: The refinement calculator: Proof support for program refinement. In: Formal Methods Pacific (1997)
Chen, W., Warren, D.S.: Tabled evaluation with delaying for general logic programs. J. ACM 43(1), 20–74 (1996)
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 2nd edn. MIT Press and McGraw-Hill (2001)
de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
de Moura, L., Bjørner, N.: Generalized, efficient array decision procedures. In: Formal Methods in Computer-Aided Design (November 2009)
Demsky, B., Rinard, M.C.: Automatic detection and repair of errors in data structures. In: OOPSLA, pp. 78–95 (2003)
Demsky, B., Rinard, M.C.: Data structure repair using goal-directed reasoning. In: ICSE, pp. 176–185 (2005)
Dutertre, B., de Moura, L.: The Yices SMT solver (2006), http://yices.csl.sri.com/tool-paper.pdf
Elkarablieh, B., Khurshid, S.: Juzi: a tool for repairing complex data structures. In: ICSE, pp. 855–858 (2008)
Elkarablieh, B., Khurshid, S., Vu, D., McKinley, K.S.: Starc: static analysis for efficient repair of complex data. In: OOPSLA, pp. 387–404 (2007)
von Essen, C., Jobstmann, B.: Program repair without regret. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 896–911. Springer, Heidelberg (2013)
Flener, P., Partridge, D.: Inductive programming. Autom. Softw. Eng. 8(2), 131–137 (2001)
Gallagher, J., Peralta, J.: Regular tree languages as an abstract domain in program specialisation. Higher-Order and Symbolic Computation 14(2-3), 143–172 (2001)
Gligoric, M., Gvero, T., Jagannath, V., Khurshid, S., Kuncak, V., Marinov, D.: Test generation through programming in UDITA. In: International Conference on Software Engineering (ICSE) (2010)
Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: PLDI, pp. 62–73 (2011)
Hanus, M.: Type-oriented construction of web user interfaces. In: PPDP, pp. 27–38 (2006)
Hanus, M., Kluß, C.: Declarative programming of user interfaces. In: Gill, A., Swift, T. (eds.) PADL 2009. LNCS, vol. 5418, pp. 16–30. Springer, Heidelberg (2008)
Hofmann, M.: IgorII - an analytical inductive functional programming system (tool demo). In: PEPM, pp. 29–32 (2010)
Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256–290 (2002)
Jacobs, S., Kuncak, V., Suter, P.: Reductions for synthesis procedures. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 88–107. Springer, Heidelberg (2013)
Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: FMCAD (2006)
Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.: Anzu: A tool for property synthesis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 258–262. Springer, Heidelberg (2007)
Kahsai, T., Tinelli, C.: PKIND: A parallel k-induction based model checker. In: 10th Int. Workshop Parallel and Distributed Methods in verifiCation, PDMC 2011 (2011)
Kitzelmann, E., Schmid, U.: Inductive synthesis of functional programs: An explanation based generalization approach. JMLR 7, 429–454 (2006)
Kneuss, E., Kuncak, V., Kuraj, I., Suter, P.: On integrating deductive synthesis and verification systems. Technical Report EPFL-REPORT-186043, EPFL (2013)
Köksal, A.S., Kuncak, V., Suter, P.: Scala to the power of Z3: Integrating SMT and programming. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 400–406. Springer, Heidelberg (2011)
Köksal, A., Kuncak, V., Suter, P.: Constraints as control. In: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL (2012)
Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: ACM SIGPLAN Conf. Programming Language Design and Implementation, PLDI (2010)
Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Functional synthesis for linear arithmetic and sets. Software Tools for Technology Transfer (STTT), TBD (TBD) (2012)
Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Software synthesis procedures. Communications of the ACM (2012)
Leino, K.R.M.: This is Boogie 2. Manuscript KRML 178, working draft (June 24, 2008)
Malik, M.Z., Siddiqui, J.H., Khurshid, S.: Constraint-based program debugging using data structure repair. ICST, 190–199 (2011)
Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst. 2(1), 90–121 (1980)
Manna, Z., Waldinger, R.J.: Toward automatic program synthesis. Commun. ACM 14(3), 151–165 (1971)
Michael Hanus, E.: Curry: An integrated functional logic language vers. 0.8.2 (2006), http://www.curry-language.org
Milicevic, A., Rayside, D., Yessenov, K., Jackson, D.: Unifying execution of imperative and declarative code. In: ICSE, pp. 511–520 (2011)
Muggleton, S., Raedt, L.D.: Inductive logic programming: Theory and methods. J. Log. Program. 19(20), 629–679 (1994)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Odersky, M.: Contracts for Scala. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 51–57. Springer, Heidelberg (2010)
Okasaki, C.: Purely Functional Data Structures. Cambridge University Press (1998)
Pei, Y., Wei, Y., Furia, C.A., Nordio, M., Meyer, B.: Evidence-based automated program fixing. CoRR, abs/1102.1059 (2011)
Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364–380. Springer, Heidelberg (2006)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL 1989: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179–190. ACM, New York (1989)
Polikarpova, N., Furia, C.A., West, S.: To run what no one has run before. In: Int. Conf. Runtime Verification (2013)
Samimi, H., Aung, E.D., Millstein, T.: Falling back on executable specifications. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 552–576. Springer, Heidelberg (2010)
Schrijvers, T., Stuckey, P.J., Wadler, P.: Monadic constraint programming. J. Funct. Program. 19(6), 663–697 (2009)
Senni, V., Fioravanti, F.: Generation of test data structures using constraint logic programming. In: Brucker, A.D., Julliand, J. (eds.) TAP 2012. LNCS, vol. 7305, pp. 115–131. Springer, Heidelberg (2012)
Singh, R., Gulwani, S.: Synthesizing number transformations from input-output examples. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 634–651. Springer, Heidelberg (2012)
Smith, D.R.: Generating programs plus proofs by refinement. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 182–188. Springer, Heidelberg (2008)
Solar-Lezama, A., Arnold, G., Tancau, L., Bodík, R., Saraswat, V.A., Seshia, S.A.: Sketching stencils. In: PLDI, pp. 167–178 (2007)
Solar-Lezama, A., Jones, C.G., Bodík, R.: Sketching concurrent data structures. In: PLDI (2008)
Solar-Lezama, A., Tancau, L., Bodík, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS (2006)
Srivastava, S., Gulwani, S., Foster, J.: From program verification to program synthesis. In: POPL (2010)
Summers, P.D.: A methodology for LISP program construction from examples. JACM 24(1), 161–175 (1977)
Suter, P.: Programming with Specifications. PhD thesis, EPFL (December 2012)
Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: ACM POPL (2010)
Suter, P., Köksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 298–315. Springer, Heidelberg (2011)
Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007)
Udupa, A., Raghavan, A., Deshmukh, J., Mador-Haim, S., Martin, M., Alur, R.: Transit: Specifying protocols with concolic snippets. In: ACM Conference on Programming Language Design and Implementation (2013)
Van Roy, P.: Logic programming in Oz with Mozart. In: ICLP (1999)
Vechev, M., Yahav, E., Yorsh, G.: Inferring synchronization under limited observability. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 139–154. Springer, Heidelberg (2009)
Wei, Y., Furia, C.A., Kazmin, N., Meyer, B.: Inferring better contracts. In: ICSE (2011)
Wei, Y., Pei, Y., Furia, C.A., Silva, L.S., Buchholz, S., Meyer, B., Zeller, A.: Automated fixing of programs with contracts. In: Proceedings of the 19th International Symposium on Software Testing and Analysis, ISSTA 2010, pp. 61–72 (2010)
Wirth, N.: Program development by stepwise refinement. Commun. ACM 26(1), 70–74 (1983) (reprint)
Nokhbeh Zaeem, R., Khurshid, S.: Contract-based data structure repair using alloy. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 577–598. Springer, Heidelberg (2010)
Zaeem, R.N., Malik, M.Z., Khurshid, S.: Repair abstractions for more efficient data structure repair. In: Int. Conf. Runtime Verification (2013)
Zee, K., Kuncak, V., Taylor, M., Rinard, M.: Runtime checking for program verification. In: Sokolsky, O., Taşıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 202–213. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kuncak, V., Kneuss, E., Suter, P. (2013). Executing Specifications Using Synthesis and Constraint Solving. In: Legay, A., Bensalem, S. (eds) Runtime Verification. RV 2013. Lecture Notes in Computer Science, vol 8174. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40787-1_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-40787-1_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40786-4
Online ISBN: 978-3-642-40787-1
eBook Packages: Computer ScienceComputer Science (R0)