The Isabelle proof assistant comes equipped with a very powerful tactic for term simplification. While tremendously useful, the results of simplifying a term do not always match the user’s expectation: sometimes, the resulting term is not in the form the user expected, or the simplifier fails to apply a rule. We describe a new, interactive tracing facility which offers insight into the hierarchical structure of the simplification with user-defined filtering, memoization and search. The new simplifier trace is integrated into the Isabelle jEdit Prover IDE.
The Prolog implementation provides a tracing facility for queries [ 2.9, 4.38] fruehwirth2012swi . An example for the tracing output can be seen in Fig. (the term creep denotes continuing the normal process). A discussion of tracing in Prolog can be found in [ 8] clocksin2003programming , and further analyses in @cite_10 . SWI uses a slightly extended variant thereof.
@cite_10
2036292005
Abstract Programming environments are essential for the acceptance of programming languages. This survey emphasizes that program analysis, both static and dynamic, is the central issue of programming environments. Because their clean semantics makes powerful analysis possible, logic programming languages have an indisputable asset in the long term. This survey is focused on logic program analysis and debugging. The large number of references provided show that the field, although maybe scattered, is active. A unifying framework is given which separates environment tools into extraction, analysis, and visualization. It facilitates the analysis of existing tools and should give some guidelines to develop new ones. Achievements in logic programming are listed; some techniques developed for other languages are pointed out, and some trends for further research are drawn. Among the main achievements are algorithmic debugging, tracing for sequential Prolog, and abstract interpretation. The main missing techniques are slicing, test case generation, and program mutation. The perspectives we see are integration, evaluation, and above all, automated static and dynamic analysis.