×

zbMATH — the first resource for mathematics

Synthesis of positive logic programs for checking a class of definitions with infinite quantification. (English) Zbl 1353.68050
The framework is based on typed first-order logic theories such as the following:
Types:
Nat generated by \(\mathrm{zero}:\rightarrow\mathrm{Nat}\quad\mathrm{succ}:\mathrm{Nat}\rightarrow\mathrm{Nat}\)
Seq generated by \(\mathrm{empty}:\rightarrow\mathrm{Seq}\quad\mathrm{succ}:\mathrm{Nat}\times\mathrm{Seq}\rightarrow\mathrm{Seq}\)

Predicates:
\(\mathrm{id}:\mathrm{Nat}\times\mathrm{Nat}\) axiomatised as:
\(\mathrm{id}(\mathrm{zero},\mathrm{zero})\Leftrightarrow \mathrm{true}\)
\(\forall(\mathrm{id}(\mathrm{succ}(X),\mathrm{zero})\Leftrightarrow\mathrm{false})\)
\(\forall(\mathrm{id}(\mathrm{zero},\mathrm{succ}(Y)\Leftrightarrow\mathrm{false})\)
\(\forall(\mathrm{id}(\mathrm{succ}(X),\mathrm{succ}(Y))\Leftrightarrow\mathrm{id}(X,Y))\)
\(\mathrm{member}:\mathrm{Nat}\times\mathrm{Seq}\) axiomatised as:
\(\forall(\mathrm{member}(E,\mathrm{empty})\Leftrightarrow\mathrm{false})\)
\(\forall(\mathrm{member}(E,\mathrm{seq}(X,Y ))\Leftrightarrow\mathrm{id}(E,X)\vee\mathrm{member}(E,Y ))\)
The authors consider assertion definitions of the form \(\forall X(r(X)\Leftrightarrow Q Y R(X,Y))\) where \(r\) is the defined relation, \(Q\) is a quantifier, and \(R\) is the defining relation, namely, a quantifier-free formula in the language of the typed first-order logic theory. For example, the following is an assertion definition for the subset relation: \[ \forall L,S(\mathrm{subset}(L,S)\Leftrightarrow\forall E(\mathrm{member}(E,L)\Rightarrow\mathrm{member}(E,S))) \] The purpose of the paper is a method to synthesise a positive logic program for checking assertions of the form \(r(X)\theta\), where \(\theta\) is a ground substitution for \(X\), that depends on the quantifier \(Q\) in such a way that if \(Q\) is \(\forall\) then the program searches for refutations, whereas if \(Q\) is \(\exists\) then the program searches for proofs. The method satisfies both key requirements:
the synthesis process terminates after a finite amount of transformation steps;
the synthesised program preserves total correctness w.r.t. the class of goals of the form \(\Leftarrow r(X,Y)\theta\).

With the example of the subset relation, the synthesised program is: \[ \begin{aligned} \forall(\mathrm{subset}(L,S) \Leftarrow \mathrm{subset}_1(E,L,S))\\ \forall(\mathrm{subset}_1(E,\mathrm{seq}(X,Y ),S) \Leftarrow \mathrm{subset}_2(E,S)\wedge \mathrm{subset}_3(E,X))\\ \forall(\mathrm{subset}_1(E,\mathrm{seq}(X,Y ),S)\Leftarrow \mathrm{subset}_1(E,Y ,S)\wedge \mathrm{subset}_4(E,X))\\ \forall(\mathrm{subset}_1(E,\mathrm{empty},S) \Leftarrow \mathrm{subset}_5(E,S))\\ \forall(\mathrm{subset}_2(E,\mathrm{seq}(X,Y )) \Leftarrow \mathrm{subset}_2(E,Y )\wedge \mathrm{subset}_4(E,X))\\ \forall(\mathrm{subset}_2(E,\mathrm{empty}) \Leftarrow \mathrm{subset}_7)\\ \mathrm{subset}_3(\mathrm{zero},\mathrm{zero}) \Leftarrow \mathrm{subset}_9\\ \forall(\mathrm{subset}_3(\mathrm{succ}(X),\mathrm{succ}(Y )) \Leftarrow \mathrm{subset}_3(X,Y ))\\ \forall(\mathrm{subset}_4(\mathrm{zero},\mathrm{succ}(Y )) \Leftarrow \mathrm{subset}_9)\\ \forall(\mathrm{subset}_4(\mathrm{succ}(X),\mathrm{succ}(Y )) \Leftarrow \mathrm{subset}_4(X,Y ))\\ \forall(\mathrm{subset}_4(\mathrm{succ}(X),\mathrm{zero}) \Leftarrow \mathrm{subset}_9)\\ \forall(\mathrm{subset}_5(E,\mathrm{seq}(X,Y )) \Leftarrow \mathrm{subset}_5(E,Y )\wedge \mathrm{subset}_4(E,X))\\ \mathrm{subset}_7 \Leftarrow\\ \mathrm{subset}_9 \Leftarrow\end{aligned} \]
following a procedure that consists of 6 steps, with intermediate formulas generated on the way, in particular: \[ \begin{aligned}\forall E,L,S(\mathrm{subset}_1(E,L,S)\Leftrightarrow(\mathrm{member}(E,L)\wedge\neg\mathrm{member}(E,S)))\\ \forall(\mathrm{subset}_2(X,Y )\Leftrightarrow\mathrm{true}\wedge\neg\mathrm{member}(X,Y ))\\ \forall(\mathrm{subset}_3(X,Y )\Leftrightarrow\mathrm{id}(X,Y ))\\ \forall(\mathrm{subset}_4(X,Y )\Leftrightarrow\neg\mathrm{id}(X,Y ))\\ \forall(\mathrm{subset}_5(X,Y )\Leftrightarrow\mathrm{false}\wedge\neg\mathrm{member}(X,Y ))\\ \mathrm{subset}_6\Leftrightarrow\mathrm{false}\wedge\neg\mathrm{false}\\ \mathrm{subset}_7\Leftrightarrow\mathrm{true}\wedge\neg\mathrm{false}\\ \mathrm{subset}_8\Leftrightarrow\mathrm{true}\wedge\neg\mathrm{true}\\ \mathrm{subset}_9\Leftrightarrow\mathrm{true}\\ \mathrm{subset}_{10}\Leftrightarrow\neg\mathrm{true}\end{aligned} \] The method has been tested with many other assertion definitions, listed in the appendix, together with the proofs of termination and correctness.
MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
68N17 Logic programming
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
Eiffel; JML; SIMPLIFY; Spec#
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Apt, K. R.; Bol, R. R., Logic programming and negation: a survey, J. Log. Program., 19-20, 9-71, (1994) · Zbl 0942.68518
[2] SunTest, The Open Group Research Institute, ADL 2.0 for Java Language Reference Manual, v1.2, 1998.
[3] Basin, D.; Deville, Y.; Flener, P.; Hamfelt, A.; Nilsson, J., Synthesis of programs in computational logic, (Program Development in Computational Logic, Lect. Notes Comput. Sci., vol. 3049, (2004), Springer Berlin), 30-65 · Zbl 1080.68562
[4] Bjorner, N., Taking satisfiability to the next level with Z3, (IJCAR, (2012)), 1-8, (Abstract) · Zbl 1358.68248
[5] M. Barnett, K. Rustan M. Leino, W. Schulte, The Spec# programming system, an overview, Manuscript KRLM 136, Microsoft Research, 2004.
[6] Basin, D.; Matthews, S., Adding metatheoretic facilities to first-order theories, J. Log. Comput., 6, 6, 835-849, (1996) · Zbl 0868.03006
[7] Barbuti, R.; Mancarella, P.; Pedreschi, D.; Turini, F., A transformational approach to negation in logic programming, J. Log. Program., 8, 201-228, (1990) · Zbl 0796.68056
[8] Bjorner, N.; McMillan, K. L.; Rybalchenko, A., On solving universally quantified Horn clauses, (SAS, (2013)), 105-125
[9] Bundy, A.; Smaill, A.; Wiggins, G., The synthesis of logic programs from inductive proofs, (Computational Logic, Symposium Proceedings, (1990), Springer-Verlag), 135-149
[10] Calejo, M., Interprolog: towards a declarative embedding of logic programming in Java, (9th European Conference on Logic in Artificial Intelligence, Lisbon, (2004))
[11] Negation as failure, (Logic and Databases, (1978), Plenum Press New York), 293-322
[12] Coquant, T.; Huet, G., The calculus of constructions, Inf. Comput., 76, 2/3, 95-120, (1988) · Zbl 0654.03045
[13] Dayantis, G., Logic program derivation for a class of first-order relations, (IJCAI, (1987))
[14] Deville, Y.; Lau, K. K., Logic program synthesis, J. Log. Program., 12, 1-32, (1993)
[15] Detlefs, D.; Nelson, G.; Saxe, J. B., Simplify: a theorem prover for program checking, J. ACM, 52, 3, 365-473, (2005) · Zbl 1323.68462
[16] Deville, Y., Logic programming. systematic program development, (1990), Addison-Wesley
[17] Dijkstra, E. W., A discipline of programming, (1976), Prentice Hall · Zbl 0368.68005
[18] Dromey, G., Program derivation. the development of programs from specifications, (1989), Addison-Wesley · Zbl 0781.68084
[19] Flener, P., Logic program synthesis from incomplete information, (1995), Kluwer Academics Publishers
[20] Flener, P., Achievements and prospects of program synthesis, (Computational Logic: Logic Programming and Beyond: Essays in Honour of Robert A. Kowalski, Part I, Lect. Notes Comput. Sci., vol. 2407, (2002), Springer Berlin), 1-43 · Zbl 1012.68500
[21] Flener, P.; Lau, K. K.; Ornaghi, M., Correct schema-guided synthesis of steadfast programs, (Proc. of ASE’97, (1997), IEEE Computer Society Press), 153-160
[22] Fribourg, L., Extracting logic programs from proofs that use extended prolog execution and induction, (ICLP90, (1990), The MIT Press), 685-699
[23] Galán, F. J.; Cañete, J. M., A method for compiling and executing expressive assertions, (4th International Conference Integrated Formal Methods, Lect. Notes Comput. Sci., vol. 2999, (2004), Springer Berlin), 521-540 · Zbl 1196.68051
[24] Ge, Y.; Barrett, C.; Tinelli, C., Solving quantified verification conditions using satisfiability modulo theories, (Proceedings of the 21st International Conference on Automated Deduction, CADE ’07, Lect. Notes Artif. Intell., vol. 4603, (July 2007), Springer-Verlag Bremen, Germany), 167-182 · Zbl 1213.68376
[25] Gulwani, S.; McCloskey, B.; Tiwari, A., Lifting abstract interpreters to quantified logical domains, (POPL, (2008)), 235-246 · Zbl 1295.68085
[26] Gries, D., The science of programming, (1981), Springer-Verlag · Zbl 0472.68003
[27] Gulwani, S., Dimensions in program synthesis, (PPDP, (2010)), 13-24
[28] Hogger, C. J., Derivation of logic programs, J. ACM, 28, 372-392, (1981) · Zbl 0464.68021
[29] The jass page
[30] Man-machine-systems, (2009), design by contract for Java using JMSAssert
[31] Java technology
[32] Kanamori, T.; Fujita, H., Unfold/fold logic program transformation with counters, (1986), ICOT Tech. Report TR-179
[33] Kramer, R., Icontract: the Java(tm) design by contract(tm) tool, (Proceedings of the Technology of Object-Oriented Languages and Systems, (1998))
[34] Kunen, K., Signed data dependencies in logic programs, J. Log. Program., 7, 231-245, (1989)
[35] Lau, K.; Ornaghi, M., On specification frameworks and deductive synthesis of logic programs, (Lect. Notes Comput. Sci., vol. 883, (1994), Springer-Verlag), 104-121
[36] Leavens, G.; Baker, A.; Ruby, C., Preliminary design of JML: a behavioral interface specification language for Java, ACM SIGSOFT Softw. Eng. Notes, 31, 3, 1-38, (March 2006)
[37] Lloyd, J. W., Foundations of logic programming, (1987), Springer-Verlag · Zbl 0547.68005
[38] Maher, M. J., A transformation system for deductive database modules with perfect models semantics, (Proc. 9th Conf. on Foundations of Software Technology and Theoretical Computer Science, (1989)), 89-98
[39] Manna, Z., Mathematical theory of computation, McGraw-Hill Comput. Sci. Ser., (1974), McGraw-Hill · Zbl 0353.68066
[40] Meyer, B., Eiffel: the language, (1992), Prentice Hall · Zbl 0779.68013
[41] de Moura, L.; Bjørner, N., Satisfiability modulo theories: introduction and applications, Commun. ACM, 54, 9, 69-77, (2011)
[42] Manna, Z.; Waldinger, R., The logical basis for computer programming. volume 1: deductive reasoning, (1985), Addison-Wesley · Zbl 0572.68008
[43] Manna, Z.; Waldinger, R., The deductive foundations of computer programming, (1993), Addison-Wesley · Zbl 0846.68013
[44] Nonnengart, A.; Weidenbach, C., Computing small clause normal forms, (Handbook of Automated Reasoning, (1999), Elsevier Science Publishers B.V.) · Zbl 0992.03018
[45] Partsch, H. A., Specification and transformation of programs. A formal approach to software development, (1990), Springer-Verlag · Zbl 0751.68036
[46] Parr, Terence, ANTLR, another tool for language recognition
[47] Pettorossi, A.; Proietti, M., Synthesis and transformation of logic programs using unfold/fold proof, J. Log. Program., 41, 197-230, (1999) · Zbl 0944.68024
[48] Pettorossi, A.; Proietti, M., Perfect model checking via unfold/fold transformations, (September, 2000), Technical report R.513 IASI-CNR, Rome
[49] Pettorossi, A.; Proietti, M., Program derivation = rules + strategies, (Computational Logic, Lect. Notes Artif. Intell., vol. 2047, (2002)), 273-309 · Zbl 1012.68033
[50] Plosch, R., Evaluation of assertion support for the Java programming language, J. Object Technol., 1, (2002)
[51] Proietti, M.; Pettorossi, A., Unfolding-definition-folding, in this order, for avoiding unnecessary variables in logic programs, Theor. Comput. Sci., 142, 89-124, (1995) · Zbl 0873.68023
[52] Sato, T., Completed logic programs and their consistency, J. Log. Program., 9, 33-44, (1990) · Zbl 0715.68011
[53] Sato, T., Equivalence-preserving first-order unfold/fold transformation systems, Theor. Comput. Sci., 105, 57-84, (1992) · Zbl 0798.68101
[54] Sato, T.; Tamaki, H., First-order compiler: a deterministic logic program synthesis algorithm, J. Symb. Comput., 8, 605-627, (1989) · Zbl 0693.68017
[55] Seki, H., Unfold/fold transformation of general logic programs for the well-founded semantics, J. Log. Program., 16, 5-23, (1993) · Zbl 0776.68031
[56] Srivastava, S.; Gulwani, S., Program verification using templates over predicate abstraction, (PLDI, (2009)), 223-234
[57] Srivastava, S.; Gulwani, S.; Chaudhuri, S.; Foster, J. S., Path-based inductive synthesis for program inversion, (PLDI, (2011)), 492-503
[58] Srivastava, S.; Gulwani, S.; Foster, J. S., From program verification to program synthesis, (POPL, (2010)), 313-326 · Zbl 1312.68068
[59] Srivastava, S.; Gulwani, S.; Foster, J. S., Template-based program verification and program synthesis, Int. J. Softw. Tools Technol. Transf., 15, 497-518, (2013)
[60] Solar-Lezama, A.; Arnold, G.; Tancau, L.; Bodík, R.; Saraswat, V. A.; Seshia, S. A., Sketching stencils, (PLDI, (2007)), 167-178
[61] Sun microsystems, programming with assertions, (2002)
[62] SWI prolog · Zbl 1244.68023
[63] Tamaki, H.; Sato, T., Unfold/fold transformation of logic programs, (Proc. 2nd International Logic Program Conference, (1984)), 127-137
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.