1: \NeedsTeXFormat{LaTeX2e}
2: \documentclass[runningheads]{llncs}
3: % -*-Mode: LaTeX; tab-width: 3; -*-
4: %\documentclass{llncs}
5: %\usepackage{isolatin1}
6:
7: \usepackage{epsfig}
8:
9: %\usepackage{hyperref}
10: \def\href#1#2{#2}
11:
12:
13: %\pagestyle{myheadings}
14:
15: %\input{prolog.sty}
16: \newcommand{\progfont}[0]{\rm\small}
17: \newcommand{\Upipe}[0]{\(|\)}
18: \newcommand{\Uoutputannotation}[0]{\(<\!\!<\!\!<\)}
19: \newcommand{\Urule}[0]{\(\leftarrow\)}
20: \newcommand{\UIrule}[0]{\(%
21: \stackrel{\scriptscriptstyle\infty}{\leftarrow}\)}
22: \newcommand{\UInrule}{\(
23: \not\stackrel{\scriptscriptstyle\infty}{\leftarrow}\)}
24: \newcommand{\ULongrightarrow}[0]{\(\Longrightarrow\)}
25: \newcommand{\ULeftrightarrow}[0]{\(\Leftrightarrow\)}
26: \newcommand{\Unotunify}[0]{\(\backslash\!\!\!=\)}
27: \newcommand{\Unrule}{\(\not\leftarrow\)}
28: \newcommand{\Udoublequote}{"{}}
29: \newcommand{\Uparagraphe}{\P}
30:
31: \def\K#1{{%
32: \progfont{%
33: #1}}} % Program text
34:
35: \newlength{\danach}
36: \newlength{\davor}
37: \def\durch#1{%
38: \settowidth{\davor}{#1}%
39: {\makebox[0pt][l]{#1}%
40: \makebox[0pt][l]{\raisebox{.4ex}{\makebox[\davor]{\hrulefill}}}%
41: \makebox[0pt][l]{\raisebox{.8ex}{\makebox[\davor]{\hrulefill}}}%
42: \raisebox{1.2ex}{\makebox[\davor]{\hrulefill}}%
43: }}
44:
45: \def\unterstrichen#1{%
46: \settowidth{\davor}{#1}%
47: {\makebox[0pt][l]{#1}%
48: \raisebox{-.5ex}{\makebox[\davor]{\hrulefill}}%
49: }}
50:
51: \newcommand{\prologcodefont}[0]{\progfont}
52: \newcommand{\internneuezeile}[0]{\\[0pt]\prologcodefont}
53: \newcommand{\interntabulator}[0]{\>\prologcodefont}
54: \newcommand{\prologcode}[0]{\prologcodefont}
55:
56: \newenvironment{Pro}[0]% Prolog und C
57: {\quad\begin{minipage}[t]{40ex}%
58: \prologcode%
59: \begin{tabbing}%
60: \hspace{3ex}\=\hspace{3ex}\=\hspace{3ex}\=\hspace{3ex}\=%
61: \hspace{6ex}\=\hspace{6ex}\=\hspace{6ex}\=\hspace{6ex}\=%
62: \hspace{6ex}\=\hspace{6ex}\=\hspace{6ex}\=\hspace{3ex}\kill}%
63: {\end{tabbing}%
64: \end{minipage}%
65: }
66: %% end prolog.sty
67:
68: \begin{document}
69:
70: \setcounter{page}{77}
71: \title{Declarative program development in Prolog with GUPU}
72: \titlerunning{Declarative program development in Prolog with GUPU}
73: \author{Ulrich Neumerkel \and Stefan Kral}
74: \authorrunning{U. Neumerkel, S. Kral}
75: \institute{Institut f{\"u}r Computersprachen\\
76: Technische Universit{\"a}t Wien, Austria,\\
77: \email{ulrich@complang.tuwien.ac.at skral@complang.tuwien.ac.at}}
78:
79: \maketitle
80:
81: \addtocounter{footnote}{1}
82: \footnotetext{In Alexandre Tessier (Ed), proceedings of the 12th International Workshop on Logic Programming Environments (WLPE 2002), July 2002, Copenhagen, Denmark.\\Proceedings of WLPE 2002: \texttt{http://xxx.lanl.gov/html/cs/0207052} (CoRR)}
83:
84: \begin{abstract}
85:
86: We present GUPU, a side-effect free environment specialized for
87: programming courses. It seamlessly guides and supports students
88: during all phases of program development, covering specification,
89: implementation, and program debugging. GUPU features several
90: innovations in this area. The specification phase is supported by
91: reference implementations augmented with diagnostic facilities.
92: During implementation, immediate feedback from test cases and from
93: visualization tools helps the programmer's program understanding. A
94: set of slicing techniques narrows down programming errors. The whole
95: process is guided by a marking system.
96:
97: \end{abstract}
98:
99: \section*{Introduction}
100:
101: Teaching logic programming has specific opportunities different from
102: traditional languages. In particular, the declarative notions can be
103: liberated from theoretical confines and be applied to actual program
104: development. Our approach is centered around the programming course
105: environment GUPU used for introductory Prolog programming courses
106: since 1992 at TU~Wien and other universities. The language used by
107: GUPU is the monotone pure subset of Prolog which also contains the
108: many constraint extensions offered by SICStus Prolog.
109:
110: In this article, we focus on the program development process supported
111: by GUPU. To illustrate this process, we will develop the predicate
112: \K{alldifferent/1} describing a list of pairwise different elements.
113:
114: The actual programming effort is divided into two stages which both
115: are equipped with appropriate diagnosing facilities. The first stage
116: (Sect.~1) is devoted to specifying a predicate by example. Cases are
117: stated where the predicate should succeed, fail, terminate, or not
118: terminate. In the second stage (Sect.~2), the actual predicate is
119: implemented and immediately tested against the previously stated
120: example cases. The whole development process is guided by a marking
121: system that highlights missing items and computes an interval
122: percentage of the fulfillment of an exercise.
123:
124: \section{Specification by example}
125:
126: Writing test cases prior to actual coding is good practice also in
127: other programming languages. It has reached broader attention with
128: the rise of the extreme programming movement~\cite{XP}. The major
129: advantage generally appreciated is increased development speed due to
130: the following reasons. Test cases are an unambiguous (albeit
131: incomplete) specification. They influence system design, making it
132: better testable. They provide immediate feedback during coding, which
133: is most important in our context. And finally, they constitute a
134: solid starting point for documentation.
135:
136: In the context of logic programming, there are several further aspects
137: in favor of this approach. Test cases focus the attention on the
138: meaning of the predicate avoiding procedural details. In particular,
139: recursive predicates are a constant source of misunderstandings for
140: students, because they confuse the notion of termination condition in
141: imperative languages with Prolog's more complex mechanisms. While
142: there is only a single notion of termination in procedural languages,
143: Prolog has two: Existential and universal termination. By writing
144: tests prior to coding, the student's attention remains focused on the
145: use of a predicate. With logic variables, test cases are more
146: expressive than in imperative languages. We can use these variables
147: existentially (in positive queries) as well as universally (in
148: negative queries).
149:
150: In our attempt to develop \K{alldifferent/1} describing a list of
151: pairwise different elements, we start by writing the following two
152: assertions. The first is a positive assertion. It ensures that there
153: must be at least a single solution for \K{alldifferent/1}. The second
154: is a negative one which insists that the given goal is not the case.
155: Here, \K{alldifferent/1} should not be true for a list with its two
156: elements being equal. Both tests cannot be expressed in traditional
157: languages.
158:
159: \begin{Pro}%
160: \Urule{} alldifferent(Xs).\internneuezeile
161: \Unrule{} alldifferent([X,X]).\internneuezeile
162: {\bf @! Definition of alldifferent/1 missing in above assertions}%
163: \end{Pro}
164:
165: \noindent
166: We write test cases directly into the program text. Upon saving, GUPU
167: inserts feedback {\em into} that text. Above, GUPU added the line
168: starting with {\bf @} to remind us that we have not yet defined
169: \K{alldifferent/1}.
170:
171: Taking all of the aforementioned advantages into account, this
172: methodology appears preferable to the traditional ``code then test''
173: approach. Still, students prefer to write code prior to testing. It
174: seems that the biggest obstacle is a lack of motivation. Test cases
175: as such do not provide any immediate feedback when they are written.
176: Why should one write tests when they might be incorrect? Such
177: incorrect tests would be misleading in the later development. For
178: this reason GUPU tests assertions for validity.
179:
180: \subsection{Reference implementation}
181:
182: All test cases provided by the student are tested against a reference
183: implementation which is realized with otherwise inaccessible
184: predicates. It is considered to be correct for those cases where the
185: reference predicate fails finitely or succeeds unconditionally. In
186: all other cases (exceptions, non-termination, pending constraints),
187: the reference implementation is incomplete and therefore unspecified
188: as discussed in the sequel.
189:
190: Cases detected as incompatible with the reference implementation are
191: highlighted immediately. In this manner, it is possible to ``test the
192: tests'' without any predicate yet defined by the student. Errors due
193: to the reference implementation start with \K{!=} to distinguish them
194: from other errors.
195:
196: We continue with the specification of \K{alldifferent/1}, by adding
197: further positive and negative assertions. In the cases below GUPU
198: disagrees and offers help.
199:
200: \begin{Pro}%
201: \Urule{} alldifferent([a,b,c,d,c]).\internneuezeile
202: {\bf != Should be negative. Details with DO on the arrow}\internneuezeile
203: \internneuezeile
204: \Unrule{} alldifferent([X,Y\Upipe{}\_]).\internneuezeile
205: {\bf != Should be positive. Details with DO on the arrow}%
206: \end{Pro}
207:
208: \subsection{Diagnosis of incorrect assertions}
209:
210: A more elaborate explanation on why an assertion is incorrect is
211: obtained on demand as proposed by the message ``DO on the arrow''
212: above. According to the kind of assertion the following steps are
213: taken. In case of an incorrect negative assertion, a more specific
214: query is produced if possible. For incorrect positive assertions, a
215: generalized query is given. In this manner, GUPU provides a detailed
216: diagnosis without showing the actual code of the reference
217: implementation. Moreover, further assertions are offered that will
218: improve test coverage during coding.
219:
220: \paragraph{Explaining incorrect negative assertions.}
221:
222: If the reference implementation succeeds in a negative assertion, a
223: more specific goal is obtained using an answer substitution of the
224: reference implementation. All free variables are grounded with new
225: constants \K{any1, any2, ...}.
226:
227: Below, an answer substitution completed the end of the list with
228: \K{[]}, and the variables \K{X} and \K{Y} have been grounded to
229: constants. GUPU temporarily inserts the specialized assertion into
230: the program text. By removing the leading @-signs, the assertion can
231: be added easily to the program.
232:
233: \begin{Pro}%
234: \Unrule{} alldifferent([X,Y\Upipe{}\_]).\internneuezeile
235: {\bf @@ \% != Should be a positive assertion.}\internneuezeile
236: {\bf @@ \% Also this more specific query should be true.}\internneuezeile
237: {\bf @@ \Urule{} X = any0, Y = any1, alldifferent([X,Y]).}%
238: \end{Pro}
239:
240:
241: \paragraph{Explaining incorrect positive assertions.}
242: If the reference implementation fails for a positive assertion, GUPU
243: tries to determine a generalized goal that fails as well. Generalized
244: goals are obtained by rewriting the goal (or a conjunction of goals)
245: up to a fixpoint with the following rules.
246:
247: \begin{description}
248:
249: \item[R1:] Replace a goal (in a conjunction) by true.
250:
251: \item[R2:] Replace a subterm of a goal's argument by a fresh variable
252: \K{\_}.
253:
254: \item[R3:] Replace two or more identical subterms by a new shared
255: variable.
256:
257: \item[R4:] Replace two non-unifiable subterms by new variables V1, V2
258: and add the goal \K{dif(V1, V2)}.
259:
260: \item[R5:] Replace a goal by a set of other goals that are known to
261: be implied.
262:
263: \end{description}
264:
265: \begin{Pro}%
266: \Urule{} alldifferent([a,b,c,d,c]).\internneuezeile
267: {\bf @@ \% != Should be a negative assertion}\internneuezeile
268: {\bf @@ \% @ Generalized negative assertion: \hfill--- using R1,R2}\internneuezeile
269: {\bf @@ \Unrule{} alldifferent([\_,\_,c,\_,c]).}\internneuezeile
270: {\bf @@ \% @ Further generalization: \hfill--- using R1-R4}\internneuezeile
271: {\bf @@ \Unrule{} alldifferent([\_,\_,V0,\_,V0]).}\internneuezeile
272: {\bf @@ \% @ Further generalization: \hfill --- using R1-R5}\internneuezeile
273: {\bf @@ \Unrule{} alldifferent([V0,\_,V0\Upipe{}\_]).}%
274: \end{Pro}
275:
276: \noindent
277: In our experience it is helpful to use several stages of
278: generalizations. Explanations that are easier to compute are
279: presented first. In the first stage, R1 and R2 are used, and the
280: generalization is displayed immediately. In the next stage, R1-R4 may
281: incur a significant amount of computation. In particular, R4 is often
282: expensive if the number of non-unifiable subterms is large. Note that
283: the obtained generalized goals are not necessarily optimal because of
284: the incompleteness of the reference implementation. In the above
285: example, the first generalization is sub-optimal. The optimum for R1
286: and R2 is \K{\Unrule{} alldifferent([\_,\_,c,\_,c\Upipe{}\_]).} However, our
287: reference implementation loops in this case. In the last
288: generalization, R5 applied ``\K{alldifferent([\_\Upipe{}Xs]) \ULongrightarrow{}
289: alldifferent(Xs).}'' twice. This permitted R1 to remove constant
290: \K{[]} at the end of the list.
291:
292: \subsection{Incomplete reference implementations}
293:
294: For most simple predicates, our reference implementation is capable of
295: determining the truth of all simple assertions. There are, however,
296: several situations where no feedback is provided.
297:
298: \begin{itemize}
299: \item The reference implementation takes too long, although most
300: reference predicates take care of many situations and are therefore
301: more complex than the student's code.
302:
303: \item The predicate itself is under-specified. Many under-specified
304: predicates, however, still allow for partial assertion testing.
305:
306: \end{itemize}
307:
308: \noindent
309: The former situation has been illustrated previously with
310: \K{alldifferent([\_,\_,c,\_,c\Upipe{}\_])}. For the latter, consider a
311: family database, the usual introductory example. While the particular
312: persons occurring in \K{child\_of/2} and \K{ancestor\_of/2} are not
313: fixed, there still remain many constraints imposed on them.
314:
315: \begin{enumerate}
316: \item[c1] No child has three parents.
317: \item[c2] A parent is an ancestor of its children.
318: \item[c3] The ancestor relation is irreflexive.
319: \item[c4] The ancestor relation is transitive.
320: \end{enumerate}
321:
322: We give here the actual reference implementation of \K{child\_of/2}
323: and \K{ancestor\_of/2} implemented in CHR~\cite{CHR}, a high-level
324: language to write constraint systems with simplification (\ULeftrightarrow{}) and
325: propagation rules (\ULongrightarrow{}). The definition provides two predicates
326: that can be executed together with regular predicates of the reference
327: implementation. This reference implementation cannot succeed
328: unconditionally because of the pending constraints imposed by CHR.
329: Therefore, it can only falsify positive assertions.
330:
331:
332: \begin{Pro}%
333: \% {\bf Reference implementation in CHR}\internneuezeile
334: \Urule{} use\_module(library(chr)).\internneuezeile
335: option(already\_in\_store, on). \% prevents infinite loops\internneuezeile
336: \internneuezeile
337: c1 @ child\_of(C,P1), child\_of(C,P2), child\_of(C,P3) \ULeftrightarrow{}\internneuezeile
338: {\interntabulator}{\interntabulator}{\interntabulator}true \& P1 \Unotunify{} P2, P2 \Unotunify{} P3, P1 \Unotunify{} P3 \Upipe{} false.\internneuezeile
339: c2 @ child\_of(A,B) \ULongrightarrow{} ancestor\_of(B,A).\internneuezeile
340: c3 @ ancestor\_of(A,A) \ULeftrightarrow{} false.\internneuezeile
341: c4 @ ancestor\_of(A,B), ancestor\_of(B,C) \ULongrightarrow{} ancestor\_of(A,C).\internneuezeile
342: \internneuezeile
343: \Urule{} child\_of(A,B), child\_of(B,C), A = C.\internneuezeile
344: {\bf != Should be negative.}\internneuezeile
345: \Urule{} alldifferent([P1,P2,P3]), child\_of(C,P1), child\_of(C,P2), child\_of(C,P3).\internneuezeile
346: {\bf != Should be negative.}%
347: \end{Pro}
348:
349:
350: \subsection{Termination}
351:
352: Termination properties and in particular non-termination properties
353: are often considered unrelated to the {\em declarative} meaning of a
354: program. It is perceived that ideally a program should always
355: terminate. We note that non-termination is often closely related to
356: completeness. In fact, a query {\em must not} terminate if the
357: intended meaning can only be expressed with an infinite number of
358: answer substitutions. Notice that this observation is completely
359: independent of Prolog's actual execution mechanism! No matter how
360: sophisticated an execution mechanism may be, its termination property
361: is constrained by the size of the generated answer. If this answer
362: must be infinite, non-termination is inevitable. For this reason,
363: cases of non-termination that are due to necessarily infinite sets of
364: answer substitutions can be safely stated in advance. On the other
365: hand, cases of termination always depend on the particular predicate
366: definition as well as on Prolog's execution mechanism.
367:
368: The most interesting cases of termination are those where actual
369: solutions are found. Termination is therefore expressed with two
370: assertions: A positive assertion to ensure a solution: \K{\Urule{} Goal.}
371: A negative one to ensure universal termination under Prolog's
372: simplistic left-to-right selection rule: \K{\Unrule{} Goal, false.} In
373: our particular case of \K{alldifferent/1}, we can state that
374: \K{alldifferent(Xs)} must not terminate, because there are infinitely
375: many lists as solutions. With the negative infinite assertion
376: \K{\UInrule{} Goal, false.} we state that \K{Goal} must not terminate
377: universally.
378:
379: \begin{Pro}%
380: \Urule{} alldifferent(Xs).\internneuezeile
381: \UInrule{} alldifferent(Xs), false.%
382: \end{Pro}
383:
384: When the length of the list is bounded (at most) a single answer
385: substitution for \K{alldifferent/1} is possible. Therefore, the
386: predicate could terminate if defined appropriately. In the example
387: below, the ideal answer is \K{dif(A,B)}.
388:
389: \begin{Pro}%
390: \Urule{} Xs = [A,B], alldifferent(Xs).\internneuezeile
391: \Unrule{} Xs = [A,B], alldifferent(Xs), false.%
392: \end{Pro}
393:
394:
395: \subsection{Summary}
396: In the first stage of realizing a predicate, only test cases are
397: given. The idea is to start from the most general goal and refine the
398: meaning of the predicate by adding further cases. To streamline this
399: process, their correctness is ensured with the help of an internal
400: reference implementation. It provides immediate feedback and detailed
401: diagnosis in the form of further test cases that can be added to the
402: program. Without any actual predicate code written, the learner is
403: put into the situation of formulating and reading queries generated by
404: the system. Note that in this first stage most errors remain local in
405: each query. The marking system provides overall guidance by demanding
406: various forms of assertions. E.g., a ground positive assertion,
407: non-termination annotations, etc.
408:
409: \section{Predicate definition}
410:
411: Armed with validated test cases obtained in the first stage, we are
412: now ready to implement \K{alldifferent/1}. Inconsistencies between
413: the student's test cases and implementation, are highlighted
414: immediately. Answer substitutions are tested with the reference
415: implementation, as shown in the central column of the following table.
416: Explanations based on slicing locate an error. We continue our
417: example by defining the predicate with an error in the underlined
418: part.
419:
420: \begin{Pro}%
421: alldifferent([]).\internneuezeile
422: alldifferent([X\Upipe{}Xs]) \Urule{}\internneuezeile
423: {\interntabulator}nonmember\_of(\unterstrichen{\bf Xs, X}),\internneuezeile
424: {\interntabulator}alldifferent(Xs).%
425: \end{Pro}
426: \begin{Pro}%
427: nonmember\_of(\_X, []).\internneuezeile
428: nonmember\_of(X, [E\Upipe{}Es]) \Urule{}\internneuezeile
429: {\interntabulator}dif(X, E),\internneuezeile
430: {\interntabulator}nonmember\_of(X, Es).%
431: \end{Pro}
432:
433: \begin{Pro}%
434: \Urule{} X = any1, Y = any2, alldifferent([X,Y]).\internneuezeile
435: {\bf ! Unexpected failure. Explanation with DO on the arrow.}\internneuezeile
436: \Urule{} Xs = [\_,\_], alldifferent(Xs).\internneuezeile
437: {\bf != The\,first solution is incorrect. Explanation with DO on\,the arrow.}\internneuezeile
438: \Unrule{} Xs = [\_,\_], alldifferent(Xs), false.\internneuezeile
439: {\bf ! Universal non-termination. Explanation with DO on the arrow.}%
440: \end{Pro}
441:
442: \vspace{-3ex}
443:
444: \subsection{Slicing}
445:
446: Slicing~\cite{slice-use} is a technique to facilitate the
447: understanding of a program. It is therefore of particular interest
448: for program debugging. The basic idea of slicing is to narrow down
449: the relevant part of a program text. For the declarative properties
450: insufficiency (unexpected failure) and incorrectness (unexpected
451: success), two different slicers have been realized. A further slicer
452: was realized to explain universal non-termination~\cite{uwn-ppdp}.
453: They all highlight fragments of the program where an error has to
454: reside. As long as the programmer does not modify the displayed
455: fragment, the error persists.
456:
457: \begin{enumerate}
458:
459: \item[a)] For unexpected failures, generalized program fragments are
460: produced that still fail. The program is generalized by deleting
461: some goals, indicated with a *-sign. To remove the error, the slice
462: must be generalized.
463:
464: \quad E.g., a rule \K{p \Urule{} q, r.} is generalized to \K{p \Urule{} *
465: \durch{q}, r.}
466:
467: \item[b)] In case of unexpected success, still succeeding specialized
468: fragments are obtained by inserting some goals \K{false/0} that
469: effectively remove program clauses. In order to remove the error,
470: the programmer has to specialize the remaining program fragment.
471:
472: \item[c)] For universal non-termination, slicing determines still
473: non-terminating specialized fragments. The inserted
474: \K{false/0}-goals hide all subsequent goals in a clause. If
475: \K{false/0} is inserted as the first goal, the clause is completely
476: eliminated. The remaining program fragment has to be modified in
477: order to remove non-termination. The constraint based algorithm is
478: found in~\cite{uwn-ppdp}.
479:
480: \quad E.g., \K{p \Urule{} p, q.} is specialized to \K{p \Urule{} p,
481: false, \durch{q}.}
482:
483: \end{enumerate}
484:
485: \noindent
486: GUPU generates the following slices on demand (``DO on the
487: arrow'').
488:
489: \noindent
490: %\renewcommand{\progfont}[0]{\rm\footnotesize}
491: \renewcommand{\progfont}[0]{\rm\scriptsize}
492: \begin{tabular}{l|l|l}
493: \hspace{-4ex}
494: \begin{Pro}%
495: \Urule{} X= any1, Y= any2,\internneuezeile
496: {\interntabulator}{\interntabulator}{\interntabulator}alldifferent([X,Y]).\internneuezeile
497: {\bf ! Unexpected failure.}\internneuezeile
498: \internneuezeile
499: \internneuezeile
500: \internneuezeile
501: \internneuezeile
502: {\bf ------ Explanation, ad a) ---}\internneuezeile
503: Generalized fragment fails.\internneuezeile
504: \internneuezeile
505: \Urule{} X= any1, Y= any2,\internneuezeile
506: {\interntabulator}{\interntabulator}{\interntabulator}alldifferent([X,Y]).\internneuezeile
507: alldifferent([]).\internneuezeile
508: alldifferent([X\Upipe{}Xs]) \Urule{}\internneuezeile
509: {\interntabulator}nonmember\_of(\progfont\unterstrichen{\progfont\bf Xs, X}),\internneuezeile
510: {\interntabulator}* \durch{alldifferent(Xs)}.\internneuezeile
511: \internneuezeile
512: nonmember\_of(\_X, []).\internneuezeile
513: nonmember\_of(X,[E\Upipe{}Es]) \Urule{}\internneuezeile
514: {\interntabulator}* \durch{dif(X, E)},\internneuezeile
515: {\interntabulator}* \durch{nonmember\_of(X, Es)}.%
516: \end{Pro}
517: &\hspace{-3ex}
518: \begin{Pro}%
519: \Urule{} Xs = [\_,\_], alldifferent(Xs).\internneuezeile
520: {\bf @@ \% Xs = [[],[]].\,\%\,Incorrect!}\internneuezeile
521: {\bf @@ \% Generalization}\internneuezeile
522: {\bf @@ \Unrule{} alldifferent([[],[]\Upipe{}\_]).}\internneuezeile
523: {\bf @@ \%\,Further\,generalization}\internneuezeile
524: {\bf @@ \Unrule{} alldifferent([V0,V0\Upipe{}\_]).}\internneuezeile
525: \internneuezeile
526: {\bf ------ Explanation, ad b) ------{}--}\internneuezeile
527: Specialized fragment succeeds.\internneuezeile
528: \internneuezeile
529: \Unrule{} alldifferent([V0,V0\Upipe{}\_]).\internneuezeile
530: \internneuezeile
531: alldifferent([]).\internneuezeile
532: alldifferent([X\Upipe{}Xs]) \Urule{}\internneuezeile
533: {\interntabulator}nonmember\_of(\unterstrichen{\bf Xs, X}),\internneuezeile
534: {\interntabulator}alldifferent(Xs).\internneuezeile
535: \internneuezeile
536: nonmember\_of(\_X, []).\internneuezeile
537: \durch{nonmember\_of(X, [E\Upipe{}Es]) \Urule{} false,}\internneuezeile
538: {\interntabulator}\durch{dif(X, E),}\internneuezeile
539: {\interntabulator}\durch{nonmember\_of(X, Es).}%
540: \end{Pro}
541: &\hspace{-3ex}
542: \begin{Pro}%
543: \Unrule{} Xs = [\_,\_], alldifferent(Xs),\internneuezeile
544: {\interntabulator}{\interntabulator}{\interntabulator}{\interntabulator}{\interntabulator}{\interntabulator}false.\internneuezeile
545: {\bf !\,Universal\,non-termination }\internneuezeile
546: \internneuezeile
547: \internneuezeile
548: \internneuezeile
549: \internneuezeile
550: {\bf ------ Explanation, ad c) --{}--}\internneuezeile
551: Fragment does not terminate.\internneuezeile
552: \internneuezeile
553: \Unrule{} Xs = [\_,\_], alldifferent(Xs),\internneuezeile
554: {\interntabulator}{\interntabulator}{\interntabulator}{\interntabulator}{\interntabulator}{\interntabulator}false.\internneuezeile
555: \durch{alldifferent([]) \Urule{} false.}\internneuezeile
556: alldifferent([X\Upipe{}Xs]) \Urule{}\internneuezeile
557: {\interntabulator}nonmember\_of(\unterstrichen{\bf Xs, X}), false,\internneuezeile
558: {\interntabulator}\durch{alldifferent(Xs)}.\internneuezeile
559: \internneuezeile
560: \durch{nonmember\_of(\_X, []) \Urule{} false.}\internneuezeile
561: nonmember\_of(X, [E\Upipe{}Es]) \Urule{}\internneuezeile
562: {\interntabulator}dif(X, E),\internneuezeile
563: {\interntabulator}nonmember\_of(X, Es), false.%
564: \end{Pro}
565: \end{tabular}
566: \renewcommand{\progfont}[0]{\rm\small}
567:
568: \noindent
569: In the above example, two declarative errors and a procedural error
570: yielded three different explanations. All explanations exposed some
571: part of the program where an error must reside. Reasoning about
572: errors can be further enhanced by combining the obtained explanations.
573: Under the assumption that the error can be removed with a single
574: modification of the program text, the error has to reside in the
575: intersection of the three fragments. The intersection of all three
576: fragments comprises only two lines of a total of eight lines --- the
577: head and first goal of \K{alldifferent/1}. This intersection is
578: currently not generated by GUPU.
579:
580: \begin{Pro}%
581: \durch{alldifferent([]).}\internneuezeile
582: alldifferent([X\Upipe{}Xs]) \Urule{}\internneuezeile
583: {\interntabulator}nonmember\_of(\unterstrichen{\bf Xs, X}),\internneuezeile
584: {\interntabulator}\durch{alldifferent(Xs)}.%
585: \end{Pro}
586: \begin{Pro}%
587: \durch{nonmember\_of(\_X, []).}\internneuezeile
588: \durch{nonmember\_of(X, [E\Upipe{}Es]) \Urule{}}\internneuezeile
589: {\interntabulator}\durch{dif(X, E),}\internneuezeile
590: {\interntabulator}\durch{nonmember\_of(X, Es).}%
591: \end{Pro}
592:
593: The advantages of using slicing in the context of a teaching
594: environment are manifold. The students' attention remains focused on
595: the logic programs and not on auxiliary formalisms like traces.
596: Reading program fragments proves to be a fruitful path toward program
597: understanding. Simpler and smaller parts can be read and understood
598: instead of the complete program. Further, the described techniques
599: are equally used for monotone extensions of pure Prolog programs like
600: constraints in the domain CLP(FD).
601:
602:
603: \subsection{Beyond Prolog semantics}
604:
605: The truth of infinite queries cannot be tested with the help of
606: Prolog's simplistic but often efficient execution mechanism. GUPU
607: subjects infinite queries implicitly to an improved execution
608: mechanism based on iterative deepening. In contrast to approaches
609: that exclusively rely on iterative deepening~\cite{yal}, we can
610: therefore obtain the best of both worlds: Prolog's efficiency and a
611: sometimes more complete search. In the case of negative infinite
612: queries, a simple loop checking prover is used. We are currently
613: investigating to further integrate more sophisticated techniques.
614:
615: \begin{Pro}%
616: nat(s(N)) \Urule{}\internneuezeile
617: {\interntabulator}nat(N).\internneuezeile
618: nat(0).\internneuezeile
619: \UInrule{} nat(N).\internneuezeile
620: {\bf !+$\!\!$+ Unexpected\,success.\,Remove\,/}%\internneuezeile
621: \end{Pro}
622: \
623: \begin{Pro}%
624: q \Urule{}\internneuezeile
625: {\interntabulator}q.\internneuezeile
626: \internneuezeile
627: \UIrule{} q.\internneuezeile
628: {\bf !+$\!\!$+ Unexpected\,failure.\,Add\,/}%
629: \end{Pro}
630:
631:
632: \subsection{Viewers}
633:
634: In a pure logic programming environment, the only way to see the
635: result of a computation is via answer substitutions which often serves
636: as an excuse to introduce impure features and side-effects. In
637: GUPU, answer substitutions are visualized in a side-effect free manner
638: with the help of viewers. Viewers provide an alternate visual
639: representation of an answer substitution which helps to understand the
640: investigated problem. To ensure that no side effects take place,
641: viewers are only allowed in assertions of the form \K{\Urule{} {\em
642: Viewer} \Uoutputannotation{} {\em Goal}.} When querying such an assertion, an
643: answer substitution of {\em Goal} is displayed along with a separate
644: window for the viewer. {\em Viewer} is one of the predefined viewers.
645: Most complex viewers are based on the Postscript viewer which expects
646: a string describing a Postscript document. In fact, many viewers have
647: been implemented side-effect free within GUPU in student projects. We
648: present two select viewers. Further viewers are discussed
649: in~\cite{uwn-viewers}.
650:
651: \begin{Pro}%
652: \Urule{} postscript(Cs) \Uoutputannotation{} Cs = \Udoublequote{}0 0 100 100 rectfill\Udoublequote{}.\internneuezeile
653: {\bf @@ \% Cs = \Udoublequote{}0 0 100 100 rectfill\Udoublequote{}.}\internneuezeile
654: {\bf @@ \%\% One solution found.}%
655: \end{Pro}
656:
657: \paragraph{Repetitive Scheduling.} Within the context of fault-tolerant,
658: distributed hard real-time systems, the need to calculate time-rigid
659: schedules arises. Before system start up, a schedule meeting the time
660: criteria of the application is calculated. The resulting table is
661: executed at run time by the components of the system. This real-world
662: application of CLP(FD)~\cite{AE} has been integrated into GUPU. The
663: viewer \K{repsched/1} displays one particular solution to this
664: scheduling problem: \\\K{\Urule{} repsched(DB-S) \Uoutputannotation{} DB = big,
665: db\_timerigidschedule(DB,S).}
666:
667:
668: The modeled system consists of several processors and of one global
669: interconnect (a bus). During design-time, every task is assigned to
670: exactly one processor. All tasks are executed periodically and are
671: fully preemptive. Tasks communicate and synchronize by sending
672: messages. Internal messages are used for tasks on the same processor.
673: All other messages are sent over the bus.
674:
675: \noindent
676: \begin{minipage}[b]{0.49\linewidth}
677: Solutions to the scheduling problem obey several constraints. All
678: messages must be transmitted after the completion of the sending task
679: and before starting the receiving task. The bus transfers at most one
680: message at a time. Transactions (specific groups of tasks) have a
681: guaranteed maximal response time (time from the start of the earliest
682: task to the end of the last completing task). Tasks having a period
683: smaller than the period of their transaction are replicated
684: accordingly. Processors execute at most one task at a time.
685:
686: \end{minipage}
687: \hfill
688: \begin{minipage}[t]{.45\linewidth}
689: \epsfig{file=repsched,width=\linewidth}
690: \end{minipage}
691:
692: \paragraph{An agent environment.}
693:
694: Another critical issue apart from basic I/O concerns the side-effect
695: free representation of logical agents. As an example, the wumpus cave
696: has been realized, well known from introductory AI texts~\cite{aima}.
697: In this world the agent is supposed to find and rescue gold in a dark
698: cave guarded by a beast and paved with other obstacles. Only by using
699: rudimentary perception, the agent makes its way through the cave. The
700: basic functionality of the agent is represented with two predicates.
701: One for initialization of the agent's state \K{init(State)} and one to
702: describe the agent's reaction upon a perception
703: \K{percept\_action\_(Percept, Action, State0, State)}. In addition,
704: the state of the agent's knowledge can be communicated via
705: \K{maybehere\_obj\_(Position, Object, State)} which should succeed if
706: the agent believes at the current \K{State} that an \K{Object} may be
707: located at \K{Position}.
708:
709: \begin{center}
710: \begin{minipage}[t]{.48\linewidth}
711: \epsfig{file=wumpus,width=\linewidth}
712: \end{minipage}
713: \hfill
714: \begin{minipage}[t]{.42\linewidth}
715: \epsfig{file=wumpuscourse,width=\linewidth}
716: \end{minipage}
717: \end{center}
718:
719:
720: The graphical representation shows the agent depicted as an arrow
721: walking through the cave as well as the location of the objects
722: invisible to the agent. The agent's belief is represented by the
723: centered squares on each field. The agent may believe that a field is
724: free, a pit, contains gold, or is occupied by the wumpus. In the
725: picture, the agent has discovered the wumpus, a pit, and some free
726: fields. All other fields are believed to contain a free field, gold,
727: or a pit. Inconsistencies between the agent's belief and reality are
728: highlighted as depicted by the field in the upper right corner. While
729: that field is a dangerous pit, the agent believes it to be safe. The
730: left viewer only displays a single situation at a time, the other
731: viewer presents the complete course through the cave at a glance,
732: simplifying the comparison of different agents.
733:
734:
735: \paragraph{Related Work.}
736: Ushell~\cite{yal} uses iterative deepening in introductory courses.
737: GUPU resorts to better strategies only when Prolog takes too long.
738: CIAOPP~\cite{ciaopp} provides a rich assertion language (types, modes,
739: determinacy, cost, ...). It is much more expressive than GUPU's but
740: also complex to learn. Prolog~IV~\cite{prologIV} has a very sophisticated
741: assertion language which is particularily well suited for constraints.
742: Approaches to teaching Prolog with programming
743: techniques~\cite{techniques} highlight patterns otherwise invisible to
744: the inexperienced. Advice is given on the programming technique and
745: coding level~\cite{hong}. GUPU provides guidance prior to any coding
746: effort. We believe programming techniques might also be useful for
747: GUPU.
748:
749:
750: \paragraph{Acknowledgments.}
751: Our thanks go to all our tutors, Heimo Adelsberger, and the Austrian
752: Computer Society (OCG). This work was partially supported by the
753: German Bundesministerium für Bildung und Forschung. Anton Ertl, David
754: Gregg, and Franz Puntigam provided valuable comments.
755:
756: \begin{thebibliography}{10}
757:
758: \bibitem{XP} K.~Beck. Extreme Programming explained, Addison-Wesley,
759: 1999.
760:
761: \bibitem{techniques}P.~Brna, A.~Bundy, T.~Dodd, M.~Eisenstadt,
762: C.K.~Looi, H.~Pain, D.~Robertson, B.~Smith, M.~van Someren. Prolog
763: programming techniques. Instructional Science 20. 1991.
764:
765: \bibitem{AE} A.~Ertl. Coroutining und Constraints in der
766: Logik-Programmierung. Diploma thesis. Technische Universität Wien,
767: 1990. pp. 75--76.
768:
769: \bibitem{CHR} Th.~Fr{\"u}hwirth. Theory and Practice of Constraint
770: Handling Rules, JLP 37, 1998.
771:
772: \bibitem{ciaopp}M.~V.~Hermenegildo, F.~Bueno, G.~Puebla,
773: P.~López. Program Analysis, Debugging, and Optimization Using
774: the Ciao System Preprocessor. Tutorial ICLP'99.
775:
776: \bibitem{hong} J. Hong. Tutoring Prolog Novices Based on Programming
777: Techniques. Intelligent Tutoring Systems 1998.
778:
779: %\bibitem{naish-type} L.~Naish. Types and the Intended Meaning of
780: % Logic. In F.~Pfenning (ed.) Types in Logic Programming, 1992,
781: % MIT-Press.
782:
783: \bibitem{uwn-ppdp} U.~Neumerkel, F.~Mesnard.
784: \href{http://www.complang.tuwien.ac.at/ulrich/papers/PDF/1999-ppdp-corr.pdf}{Localizing
785: and explaining reasons for nonterminating logic programs with
786: failure slices}. PPDP. 1999.
787:
788: \bibitem{uwn-viewers} U.~Neumerkel, Ch.~Rettig, Ch.~Schallhart.
789: \href{http://www.complang.tuwien.ac.at/ulrich/papers/PDF/wlpe97.pdf}{Visualizing
790: Solutions with Viewers}, WLPE. 1997.
791:
792: \bibitem{prologIV} PrologIA. Utilisation des Assertions dans les
793: programmes Prolog IV, Ch.~13. In Le manuel de Prolog IV.
794:
795: \bibitem{aima} S.~J.~Russel, P.~Norvig. Artificial Intelligence -- A
796: Modern Approach, Prentice Hall. 1994.
797:
798: \bibitem{slice-use} M.~Weiser. Programmers Use Slices When
799: Debugging. CACM 25(7), 446--452, 1982.
800:
801: \bibitem{yal}L.~Ü.~Yalçinalp. Ushell. Symposium on Applied Computing, 1993.
802:
803: \end{thebibliography}
804: \end{document}
805: