# 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#
Full Text:
##### References:
  Apt, K. R.; Bol, R. R., Logic programming and negation: a survey, J. Log. Program., 19-20, 9-71, (1994) · Zbl 0942.68518  SunTest, The Open Group Research Institute, ADL 2.0 for Java Language Reference Manual, v1.2, 1998.  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  Bjorner, N., Taking satisfiability to the next level with Z3, (IJCAR, (2012)), 1-8, (Abstract) · Zbl 1358.68248  M. Barnett, K. Rustan M. Leino, W. Schulte, The Spec# programming system, an overview, Manuscript KRLM 136, Microsoft Research, 2004.  Basin, D.; Matthews, S., Adding metatheoretic facilities to first-order theories, J. Log. Comput., 6, 6, 835-849, (1996) · Zbl 0868.03006  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  Bjorner, N.; McMillan, K. L.; Rybalchenko, A., On solving universally quantified Horn clauses, (SAS, (2013)), 105-125  Bundy, A.; Smaill, A.; Wiggins, G., The synthesis of logic programs from inductive proofs, (Computational Logic, Symposium Proceedings, (1990), Springer-Verlag), 135-149  Calejo, M., Interprolog: towards a declarative embedding of logic programming in Java, (9th European Conference on Logic in Artificial Intelligence, Lisbon, (2004))  Negation as failure, (Logic and Databases, (1978), Plenum Press New York), 293-322  Coquant, T.; Huet, G., The calculus of constructions, Inf. Comput., 76, 2/3, 95-120, (1988) · Zbl 0654.03045  Dayantis, G., Logic program derivation for a class of first-order relations, (IJCAI, (1987))  Deville, Y.; Lau, K. K., Logic program synthesis, J. Log. Program., 12, 1-32, (1993)  Detlefs, D.; Nelson, G.; Saxe, J. B., Simplify: a theorem prover for program checking, J. ACM, 52, 3, 365-473, (2005) · Zbl 1323.68462  Deville, Y., Logic programming. systematic program development, (1990), Addison-Wesley  Dijkstra, E. W., A discipline of programming, (1976), Prentice Hall · Zbl 0368.68005  Dromey, G., Program derivation. the development of programs from specifications, (1989), Addison-Wesley · Zbl 0781.68084  Flener, P., Logic program synthesis from incomplete information, (1995), Kluwer Academics Publishers  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  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  Fribourg, L., Extracting logic programs from proofs that use extended prolog execution and induction, (ICLP90, (1990), The MIT Press), 685-699  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  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  Gulwani, S.; McCloskey, B.; Tiwari, A., Lifting abstract interpreters to quantified logical domains, (POPL, (2008)), 235-246 · Zbl 1295.68085  Gries, D., The science of programming, (1981), Springer-Verlag · Zbl 0472.68003  Gulwani, S., Dimensions in program synthesis, (PPDP, (2010)), 13-24  Hogger, C. J., Derivation of logic programs, J. ACM, 28, 372-392, (1981) · Zbl 0464.68021  The jass page  Man-machine-systems, (2009), design by contract for Java using JMSAssert  Java technology  Kanamori, T.; Fujita, H., Unfold/fold logic program transformation with counters, (1986), ICOT Tech. Report TR-179  Kramer, R., Icontract: the Java(tm) design by contract(tm) tool, (Proceedings of the Technology of Object-Oriented Languages and Systems, (1998))  Kunen, K., Signed data dependencies in logic programs, J. Log. Program., 7, 231-245, (1989)  Lau, K.; Ornaghi, M., On specification frameworks and deductive synthesis of logic programs, (Lect. Notes Comput. Sci., vol. 883, (1994), Springer-Verlag), 104-121  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)  Lloyd, J. W., Foundations of logic programming, (1987), Springer-Verlag · Zbl 0547.68005  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  Manna, Z., Mathematical theory of computation, McGraw-Hill Comput. Sci. Ser., (1974), McGraw-Hill · Zbl 0353.68066  Meyer, B., Eiffel: the language, (1992), Prentice Hall · Zbl 0779.68013  de Moura, L.; Bjørner, N., Satisfiability modulo theories: introduction and applications, Commun. ACM, 54, 9, 69-77, (2011)  Manna, Z.; Waldinger, R., The logical basis for computer programming. volume 1: deductive reasoning, (1985), Addison-Wesley · Zbl 0572.68008  Manna, Z.; Waldinger, R., The deductive foundations of computer programming, (1993), Addison-Wesley · Zbl 0846.68013  Nonnengart, A.; Weidenbach, C., Computing small clause normal forms, (Handbook of Automated Reasoning, (1999), Elsevier Science Publishers B.V.) · Zbl 0992.03018  Partsch, H. A., Specification and transformation of programs. A formal approach to software development, (1990), Springer-Verlag · Zbl 0751.68036  Parr, Terence, ANTLR, another tool for language recognition  Pettorossi, A.; Proietti, M., Synthesis and transformation of logic programs using unfold/fold proof, J. Log. Program., 41, 197-230, (1999) · Zbl 0944.68024  Pettorossi, A.; Proietti, M., Perfect model checking via unfold/fold transformations, (September, 2000), Technical report R.513 IASI-CNR, Rome  Pettorossi, A.; Proietti, M., Program derivation = rules + strategies, (Computational Logic, Lect. Notes Artif. Intell., vol. 2047, (2002)), 273-309 · Zbl 1012.68033  Plosch, R., Evaluation of assertion support for the Java programming language, J. Object Technol., 1, (2002)  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  Sato, T., Completed logic programs and their consistency, J. Log. Program., 9, 33-44, (1990) · Zbl 0715.68011  Sato, T., Equivalence-preserving first-order unfold/fold transformation systems, Theor. Comput. Sci., 105, 57-84, (1992) · Zbl 0798.68101  Sato, T.; Tamaki, H., First-order compiler: a deterministic logic program synthesis algorithm, J. Symb. Comput., 8, 605-627, (1989) · Zbl 0693.68017  Seki, H., Unfold/fold transformation of general logic programs for the well-founded semantics, J. Log. Program., 16, 5-23, (1993) · Zbl 0776.68031  Srivastava, S.; Gulwani, S., Program verification using templates over predicate abstraction, (PLDI, (2009)), 223-234  Srivastava, S.; Gulwani, S.; Chaudhuri, S.; Foster, J. S., Path-based inductive synthesis for program inversion, (PLDI, (2011)), 492-503  Srivastava, S.; Gulwani, S.; Foster, J. S., From program verification to program synthesis, (POPL, (2010)), 313-326 · Zbl 1312.68068  Srivastava, S.; Gulwani, S.; Foster, J. S., Template-based program verification and program synthesis, Int. J. Softw. Tools Technol. Transf., 15, 497-518, (2013)  Solar-Lezama, A.; Arnold, G.; Tancau, L.; Bodík, R.; Saraswat, V. A.; Seshia, S. A., Sketching stencils, (PLDI, (2007)), 167-178  Sun microsystems, programming with assertions, (2002)  SWI prolog · Zbl 1244.68023  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.