Jamie Andrews: Some Recent Publications

Akbar Siami Namin and James H. Andrews, Finding Sufficient Mutation Operators via Variable Reduction, Proceedings of the Second Workshop on Mutation Analysis (Mutation2006), workshop at ISSRE 2006, Raleigh, NC, November 2006, 10pp.

• Abstract: A set of mutation operators is "sufficient" if it can be used for most purposes to replace a larger set. We describe in detail an experimental procedure for determining a set of sufficient C language mutation operators. We also describe several statistical analyses that determine sufficient subsets with respect to several different criteria, based on standard techniques for variable reduction. We have begun to carry out our experimental procedure on seven standard C subject programs. We present preliminary results that indicate that the procedure and analyses are feasible and yield useful information.

James H. Andrews, Lionel C. Briand, Yvan Labiche, and Akbar Siami Namin, Using Mutation Analysis for Assessing and Comparing Testing Coverage Criteria, IEEE Transactions on Software Engineering, v. 32, no. 8, August 2006, pp. 608-624.

• Abstract: The empirical assessment of test techniques plays an important role in software testing research. One common practice is to seed faults in subject software, either manually or by using a program that generates all possible mutants based on a set of mutation operators. The latter allows the systematic, repeatable seeding of large numbers of faults, thus facilitating the statistical analysis of fault detection effectiveness of test suites; however, we do not know whether empirical results obtained this way lead to valid, representative conclusions. Focusing on four common control and data flow criteria (Block, Decision, C-Use, P-Use), this paper investigates this important issue based on a middle size industrial program with a comprehensive pool of test cases and known faults.

  Based on the data available thus far, the results are very consistent across the investigated criteria, as they show that the use of mutation operators is yielding trustworthy results: generated mutants can be used to predict the detection effectiveness of real faults. Applying such mutation analysis, we then investigate the relative cost and effectiveness of the above mentioned criteria by revisiting fundamental questions regarding the relationships between fault detection, test suite size, and control/data flow coverage. Although such questions have been partially investigated in previous studies, we can use a large number of mutants which helps decrease the impact of random variation in our analysis and allows us to use a different analysis approach. Our results are then compared with published studies, plausible reasons for the differences are provided, and the research leads us to suggest a way to tune the mutation analysis process to possible differences in fault detection probabilities in a specific environment.

James H. Andrews, Susmita Haldar, Yong Lei and Felix Chun Hang Li, Tool Support for Randomized Unit Testing, Proceedings of the First International Workshop on Randomized Testing (RT'06), workshop at ISSTA 2006, Portland, Maine, July 2006, pp. 36-45.

• Abstract: There are several problem areas that must be addressed when applying randomization to unit testing. As yet no general, fully automated solution that works for all units has been proposed. We therefore have developed RUTE-J, a Java package intended to help programmers do randomized unit testing in Java. In this paper, we describe RUTE-J and illustrate how it supports the development of per-unit solutions for the problems of randomized unit testing. We report on an experiment in which we applied RUTE-J to the standard Java TreeMap class, measuring the efficiency and effectiveness of the technique. We also illustrate the use of randomized testing in experimentation, by adapting RUTE-J so that it generates randomized minimal covering test suites, and measuring the effectiveness of the test suites generated.

James H. Andrews, Susmita Haldar, Yong Lei and Chun Hang Li, Randomized Unit Testing: Tool Support and Best Practices, Technical Report No. 663, Department of Computer Science, University of Western Ontario, January 2006.

• Abstract: Randomization has long been used in testing, but it has not achieved widespread acceptance due to a lack of tool support and a failure to establish recognized best practices. In this paper, we describe RUTE-J, a Java package intended to provide tool support for randomized Java unit testing. We also discuss the best practices we have identified in our research on randomized unit testing. We report on case studies and an experiment in which we applied RUTE-J to various public-domain Java classes, finding failures even in mature software and supporting the claim that RUTE-J is an efficient, effective tool for unit testing. Finally, we compare the use of randomized unit testing to the use of other tools such as model checkers, and discuss the tradeoffs. We conclude that when best practices are followed, randomized unit testing with tool support is useful both as a preparation for full software model checking, and in its own right.

Yong Lei and James H. Andrews, Minimization of Randomized Unit Test Cases, Proceedings of the 16th International Symposium on Software Reliability Engineering (ISSRE 2005), Chicago, November 2005, pp. 267-276.

• Abstract: We describe a framework for randomized unit testing, and give empirical evidence that generating unit test cases randomly and then minimizing the failing test cases results in significant benefits. Randomized generation of unit test cases (sequences of method calls) has been shown to allow high coverage and to be highly effective. However, failing test cases, if found, are often very long sequences of method calls. We show that Zeller and Hildebrandt's test case minimization algorithm significantly reduces the length of these sequences. We study the resulting benefits qualitatively and quantitatively, via a case study on found open-source data structures and an experiment on lab-built data structures.

James H. Andrews, Lionel C. Briand and Yvan Labiche, Is Mutation an Appropriate Tool for Testing Experiments?, Proceedings of the 27th IEEE International Conference on Software Engineering (ICSE 2005), St. Louis, Missouri, May 2005, pp. 402-411.

• Abstract: The empirical assessment of test techniques plays an important role in software testing research. One common practice is to instrument faults, either manually or by using mutation operators. The latter allows the systematic, repeatable seeding of large numbers of faults; however, we do not know whether empirical results obtained this way lead to valid, representative conclusions. This paper investigates this important question based on a number of programs with comprehensive pools of test cases and known faults. It is concluded that, based on the data available thus far, the use of mutation operators is yielding trustworthy results (generated mutants are similar to real faults). Mutants appear however to be different from hand-seeded faults that seem to be harder to detect than real faults.

James H. Andrews, Lionel C. Briand and Yvan Labiche, Is Mutation an Appropriate Tool for Testing Experiments?, Technical Report No. SCE-04-15, Department of Systems and Computer Engineering, Carleton University, Ottawa, Ont., September 2004.

• Abstract: The empirical assessment of test techniques plays an important role in software testing research. One common practice is to instrument faults, either manually or by using mutation operators. The latter allows the systematic, repeatable seeding of large numbers of faults; however, we do not know whether empirical results obtained in this way lead to valid, representative conclusions. This paper investigates this important question based on a number of programs with comprehensive pools of test cases and known faults. It is concluded that, based on the data available thus far, the use of mutation operators is yielding trustworthy results.

James H. Andrews, A Case Study of Coverage-Checked Random Data Structure Testing, Proceedings of the 19th IEEE International Conference on Automated Software Engineering (ASE 2004), Linz, Austria, September 2004, pp. 316-319.

• Abstract: We study coverage-checked random unit testing (CRUT), the practice of repeatedly testing units on sequences of random function calls until given code coverage goals are achieved. Previous research has shown that this practice can be a useful complement to traditional testing methods. However, questions remained as to the breadth of its applicability.

  In this paper, we report on a case study in which we applied CRUT to the testing of two mature public-domain data structures packages. We show that CRUT helped in identifying faults, in debugging, in extracting and specifying actual behaviour, and in achieving greater assurance of the correctness of the debugged software.

  Keywords: Testing, random testing, unit testing, test oracles, empirical software engineering

James H. Andrews, Relevant Empirical Testing Research: Challenges and Responses, position paper for the Workshop on Empirical Research in Software Testing (WERST), workshop at the International Symposium on Software Testing and Analysis, Boston, MA, July 2004.

• Abstract: Empirical research on software testing that aims to be relevant to industry faces important challenges. In this position paper, we review the background on software testing research and discuss some of the most important challenges. We then give suggestions on how to respond to these challenges.

James H. Andrews, A Proof Assistant for a Weakly-Typed Higher Order Logic, Newsletter of the Association for Logic Programming (ALP), May, 2004.

• An invited, informal paper on the logical foundations and implementation of a proof assistant program based on Gilmore logic.

James H. Andrews, Coverage-Checked Random Testing of Data Structures: The Sourceforge Case Study, Technical Report No. DCS-285-IR, Department of Computer Science, University of Victoria, April 2004.

• Abstract: We study coverage-checked random unit testing (CRUT), the practice of repeatedly testing units on sequences of random function calls until given code coverage goals are achieved. Previous research has shown that this practice can be a useful complement to traditional testing methods. However, questions remain as to the breadth of applicability of the practice. In this report, we present the results of a case study into using CRUT for testing data structures. We applied CRUT to the testing of two data structures packages taken from the Sourceforge open-source code repository. Despite the maturity of the packages and the fact that they had been extensively tested, we identified faults in the units. We found that CRUT also helped in debugging, in extracting and specifying actual behaviour, and in achieving greater assurance of the correctness of the debugged software. However, we also found that some characteristics of the Sourceforge units would make our previous research on automated CRUT difficult to apply to them, such as the practical infeasibility of achieving 100% coverage.

James H. Andrews, Deriving State-Based Test Oracles for Conformance Testing, Proceedings of the Second International Workshop on Dynamic Analysis (WODA 2004), ICSE 2004 workshop, Edinburgh, Scotland, May 2004, pp. 9-16.

• Abstract: We address the problem of how to instrument code to log events for conformance testing purposes, and how to write test oracles that process log files. We specifically consider oracles written in languages based on the state-machine formalism. We describe two processes for systematically deriving logging code and oracles from requirements. The first is a process that we have used and taught, and the second is a more detailed process that we propose to increase the flexibility and traceability of the first process.

Guan Huang and James H. Andrews, Learning and Initial Use of a Software Testing Technology: An Exploratory Study, Proceedings of the 8th International Conference on Empirical Assessment in Software Engineering (EASE 2004), Edinburgh, Scotland, May 2004, pp. 77-86.

• Abstract: We describe the design, execution and results of an empirical study concerning a domain-specific language, tool and technique to facilitate software test result checking. The study was aimed at finding deficiencies in the technology itself and in the methods we used to train users in the technology. We identify several such deficiencies, and suggest remedies for the technology.

  Keywords: Testing, test oracles, test result checking, case studies, human subjects, training methods

James H. Andrews, Cut Elimination for a Weakly Typed Higher Order Logic, Technical Report No. 611, Department of Computer Science, University of Western Ontario, December 2003.

• Abstract: Cut-elimination is proved for a weakly-typed higher order logic based on those presented by Gilmore. The logic allows lambda-abstraction over terms and formulas, permitting all terms of the untyped lambda calculus including the Y combinator, and providing various methods of expressing recursive functions and predicates. Consistency is achieved in the logic via a nominalist distinction between use and mention of terms. This report is intended as a companion to Andrews, "A Weakly-Typed Logic with General Lambda Terms and Y-Combinator", Works in Progress Track, TPHOLs 2002, which presented the syntax, semantics and consistency of the logic.

James H. Andrews and Yingjun Zhang, General Test Result Checking with Log File Analysis, IEEE Transactions on Software Engineering, v. 29, no. 7, July 2003, pp. 634-648.

• Abstract: We describe and apply a lightweight formal method for checking test results. The method assumes that the software under test writes a text log file; this log file is then analyzed by a program to see if it reveals failures. We suggest a state-machine-based formalism for specifying the log file analyzer programs, and describe a language and implementation based on that formalism.
  We report on empirical studies of the application of log file analysis to random testing of units. We describe the results of experiments done to compare the performance and effectiveness of random unit testing with coverage checking and log file analysis to other unit testing procedures. The experiments suggest that writing a formal log file analyzer and using random testing is competitive with other formal and informal methods for unit testing.

James H. Andrews, Rui Fu and Vicky D. Liu, Adding Value to Formal Test Oracles, Proceedings of the 17th Automated Software Engineering Conference (ASE'02), Edinburgh, Scotland, September 2002, pp. 275-278.

• Abstract: Test oracles are programs which check the output of test cases run on other programs. We describe techniques which add value to formally-defined test oracles in three ways: (a) by measuring functional coverage of test suites, (b) by giving automated support to the process of validating the oracles, and (c) by automating the generation of test cases from the oracles. The techniques involve the use of coverage measures and AI-based search algorithms. We describe the application of these techniques in the verification and validation of a complex piece of real-world software.

James H. Andrews, A Weakly-Typed Higher Order Logic with General Lambda Terms and Y Combinator, Proceedings, Works In Progress Track, 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs '02), Hampton Roads, Virginia, August 2002, pp. 1-11, NASA Conference Publication CP-2002-211736.
And here are the PowerPoint slides of a talk I gave, related to this material, to the Logic group at the University of Ottawa, Oct. 20 2003.

• Abstract: We define a higher order logic which has only a weak notion of type, and which permits all terms of the untyped lambda calculus and allows the use of the Y combinator in writing recursive predicates. The consistency of the logic is maintained by a distinction between use and mention, as in Gilmore's logics. We give a consistent model theory and a proof system which is valid with respect to the model theory. We also give examples showing what formulas can and cannot be used in the logic.

James H. Andrews, The Witness Properties and the Semantics of the Prolog Cut, Theory and Practice of Logic Programming, v. 3, no. 1, January 2003, pp. 1-59. Also posted on the Computing Research Repository (CoRR).

• Abstract: The semantics of the Prolog ``cut'' construct is explored in the context of some desirable properties of logic programming systems, referred to as the witness properties. The witness properties concern the operational consistency of responses to queries. A generalization of Prolog with negation as failure and cut is described, and shown not to have the witness properties. A restriction of the system is then described, which preserves the choice and first-solution behaviour of cut but allows the system to have the witness properties.
  The notion of cut in the restricted system is more restricted than the Prolog hard cut, but retains the useful first-solution behaviour of hard cut, not retained by other proposed cuts such as the ``soft cut''. It is argued that the restricted system achieves a good compromise between the power and utility of the Prolog cut and the need for internal consistency in logic programming systems. The restricted system is given an abstract semantics, which depends on the witness properties; this semantics suggests that the restricted system has a deeper connection to logic than simply permitting some computations which are logical.
  Parts of this paper appeared previously in a different form in the Proceedings of the 1995 International Logic Programming Symposium.

James H. Andrews, Process-Algebraic Foundations of Aspect-Oriented Programming, Proceedings of the Third International Conference on Metalevel Architectures and Separation of Crosscutting Concerns (Reflection 2001), Kyoto, Japan, September 26-28, 2001. Springer LNCS, volume 2192, pp. 187-209. Copyright Springer-Verlag.

• Abstract: Process algebras are proposed as a foundation for aspect-oriented programming. A particular process algebra is described, and programs illustrating its use in programming are given. It is argued that the framework clarifies the notion of equivalence between programs and correctness of aspect-weaving algorithms. The question of which notion of equivalence is most appropriate is discussed from theoretical and practical points of view. An aspect-weaving algorithm is presented and proven correct. A simple imperative aspect-oriented language is presented and translated into the given process algebra.

James H. Andrews and Hanan Lutfiyya, "Experiences with a Software Maintenance Project Course", IEEE Transactions on Education, v. 43, no. 4, November 2000, pp. 383-388.

• Abstract: A report is made on an experience of teaching a senior-year course on software maintenance, centered around a maintenance project. For the course, students organized themselves into groups and worked on adaptive and perfective maintenance of selected real-world software products. The projects involved such issues as code understanding, requirements engineering, and maintenance design, and dealt with both open-source and proprietary software. The main triumphs and pitfalls of the course are recounted, and recommendations are made on project selection and general course conduct.

James H. Andrews and Yingjun Zhang, "Broad-Spectrum Studies of Log File Analysis" Proceedings of the 22nd International Conference on Software Engineering (ICSE 2000), Limerick, Ireland, June 2000, pp. 105-114. (And here are the slides of the talk I gave.)

• Abstract: This paper reports on research into applying the technique of log file analysis for checking test results to a broad range of testing and other tasks. The studies undertaken included applying log file analysis to both unit- and system-level testing and to requirements of both safety-critical and non-critical systems, and the use of log file analysis in combination with other testing methods. The paper also reports on the technique of using log file analyzers to simulate the software under test, both in order to validate the analyzers and to clarify requirements. It also discusses practical issues to do with the completeness of the approach, and includes comparisons to other recently-published approaches to log file analysis.

James H. Andrews, "Testing using Log File Analysis." The slides of a presentation at Nokia Corp., Burlington, Massachusetts, USA, Feb. 15, 2000.

James H. Andrews, "The Witness Properties and the Semantics of the Prolog Cut." Technical Report 542, Dept. of Computer Science, Univ. of Western Ontario, December 1999.

• Abstract: The semantics of the Prolog "cut" construct is explored in the context of some desirable properties of logic programming systems, referred to as the witness properties. The witness properties concern the operational consistency of responses to queries. A generalization of Prolog with negation as failure and cut is described, and shown not to have the witness properties. A restriction of the system is then described, which preserves the choice and first-solution behaviour of cut but allows the system to have the witness properties. A static analysis system is described which allows programs to be computed in a more efficient manner under the restricted system. The restricted system is then given an abstract semantics, which depends essentially on the witness properties. Finally, it is shown how the abstract semantics can be used to simplify proofs of properties of programs. Parts of this paper appeared previously in a different form in the Proceedings of the 1995 International Logic Programming Symposium.

James H. Andrews and Hanan L. Lutfiyya, "Experience Report: A Software Maintenance Project Course." Proceedings of the 13th Conference on Software Engineering Education and Training , Austin, Texas, USA, March 2000, pp. 132-139.

• Abstract: A report is made on an experience of teaching a senior-year course on software maintenance, centred around a maintenance project. The main triumphs and pitfalls are recounted, and recommendations are made on project selection and general course conduct.

James H. Andrews, Veronica Dahl, and Bharat Jayaraman, "Logic Grammars, Compositional Semantics, and Overgeneration." Proceedings of the Sixth International Workshop on Natural Language Understanding and Logic Programming , Las Cruces, New Mexico, USA, December 1999, pp. 1-16.

• Abstract: First-order treatments of long-distance phenomena such as relativization typically suffer from overgeneration. Higher order inspired extensions of Prolog have been proposed with varying degrees of success, but still suffer from overgeneration in the case of imbricated structures. We first propose an Assumption Grammar based treatment which deals successfully with this case both for analysis and for generation, and which maintains semantic compositionality as well. We then propose a cleaner, true higher order logic approach which solves the same problems, we argue that this approach is superior to other kinds of grammars dealing with long distance dependencies, and we advocate the development of a mixed platform ($\lambda$-Prolog plus continuation based assumptions) where the best of both worlds can be exploited.

James H. Andrews, "Testing using Log File Analysis." The slides of a presentation at the IBM-sponsored First International Workshop on Technological Challenges of Electronic Commerce, Markham, Ont., Canada, September 1998.

James H. Andrews, "Testing using Log File Analysis: Tools, Methods and Issues." Procs. 13th Annual International Conference on Automated Software Engineering (ASE'98), Honolulu, Hawaii, October 1998, pp. 157-166.

• Abstract: Large software systems often keep log files of events. Such log files can be analyzed to check whether a run of a program reveals faults in the system. We discuss how such log files can be used in software testing. We present a framework for automatically analyzing log files, and describe a language for specifying analyzer programs and an implementation of that language. The language permits compositional, compact specifications of software, which act as test oracles; we discuss the use and efficacy of these oracles for unit- and system-level testing in various settings. We explore methodological issues such as efficiency and logging policies, and the scope and limitations of the framework. We conclude that testing using log file analysis constitutes a useful methodology for software verification, somewhere between current testing practice and formal verification methodologies.

Richard Yates, James Andrews and Phil Gray, "Practical Experience Applying Formal Methods to Air Traffic Management Software." Procs. 8th Annual International Symposium of the International Council on Systems Engineering (INCOSE'98), Vancouver, BC, Canada, July 1998.

• Abstract: This paper relates experiences with formal methods that are relevant to the systems engineering activities of requirements specification, design documentation, and test case generation. Specifically, this paper reviews the lessons learned from the application of formal methods to selected components of an air traffic management system. This project used experimental tools developed at the University of British Columbia: S, a formal specification tool; HPP, an HTML documentation tool; and TCG, a test case generation tool. The components experimented on are from a recently fielded system written in C++ using unimplemented pre- and post-conditions on components. The purpose of the experiment was to evaluate the usefulness of these formal methods to uncover design or logic errors in the system components and to assist in designing test cases. This experience identified some ambiguities in the original specification, evaluated the feasibility of the experimental tools we used, and identified areas in which the tools could be improved.

James H. Andrews, "On the Spreadsheet Presentation of Proof Obligations." Procs. Workshop on User Interfaces in Theorem Proving (UITP'98), Eindhoven, Netherlands, July 1998, pp. 34-41.

• Abstract: A compact and structured format for presenting proof obligations is described. The format places the formulas and proof obligations in the form of a spreadsheet, where rows are formulas, columns are obligations, and cells record whether and how a formula appears in an obligation. This spreadsheet presentation frees the proof system from some interface-related restrictions, and allows users to follow a more natural style of problem solving. It can be applied to either sequent or tableau logics, and can be used by most theorem proving systems. An initial implementation is discussed, some recommendations are made for future effort, and a graphical user interface design is proposed based on the spreadsheet model.

James H. Andrews, "Theory and Practice of Log File Analysis." Technical Report 524, Dept. of Computer Science, Univ. of Western Ontario, May 1998.

• Abstract: Large software systems often keep log files of events. Such log files can be analyzed to check whether a run of a program reveals faults in the system. We discuss how such log files can be used in software testing. We present a formal framework for analyzing log files, and describe a language for specifying analyzer programs and an implementation of that language. The automated analyzers act as test oracles; we discuss the use and efficacy of these oracles for unit- and system-level testing in various settings. We explore methodological issues such as efficiency and logging policies, and the scope and limitations of the framework. We conclude that testing using log file analysis constitutes a useful methodology for software verification, whose level of rigour and ease of use is somewhere between that of current testing practice and that of formal verification methodologies.

James H. Andrews, "Prolog: Programming in Logic." Handbook of Programming Languages, volume 4, Macmillan USA, 1998. Ed. Peter Salus.

• This publication is not available via the Internet for copyright reasons.

James H. Andrews, Nancy A. Day, and Jeffrey J. Joyce, "Using a Formal Description Technique to Model Aspects of a Global Air Traffic Telecommunications Network." Procs. Formal Description Techniques / Protocol Specification, Testing and Verification (FORTE/PSTV'97), Osaka, Japan, November 1997, pub. Chapman & Hall, pp. 417-432

• Abstract: Aspects of a draft version of the Aeronautical Telecommunications Network (ATN) Standards and Recommended Practices (SARPs) under development by ISO-compliant committees of the International Civil Aviation Organization (ICAO) have been mathematically modelled using a formal description technique. The ATN SARPs are a specification for a global telecommunications network for air traffic control systems. A version of Harel's statecharts formalism embedded within a machine readable typed predicate logic has been used as a formal description technique to construct this mathematical model. Our model has been typechecked to partially validate the internal consistency of the specification. The work described in this paper has already uncovered some problems in the draft SARPs, and will provide a basis for follow-on efforts to apply formal analysis methods such as model-checking and symbolic execution to aspects of the ATN SARPs. The success of this approach suggests that typed predicate logic is useful as a syntactic and semantic foundation for specialized Formal Description Techniques (FDTs).

James H. Andrews, "Executing Formal Specifications by Translation to Higher Order Logic Programming." Procs. Theorem Proving in Higher Order Logics (TPHOLs'97), Bell Labs, New Jersey, August 1997, Springer LNCS no. 1275, pp. 17-32. Copyright Springer-Verlag.

• Abstract: We describe the construction and use of a system for translating higher order logic-based specifications into programs in the higher order logic programming language Lambda Prolog. The translation improves on previous work in the field of executing specifications by allowing formulas with quantifiers to be executed, and by permitting users to pose Prolog-style queries with free variables to be instantiated by the system. We also discuss various alternative target languages and design decisions in implementing the translator.

James Andrews, "A Logical Semantics for Depth-First Prolog with Ground Negation." Theoretical Computer Science, v. 184, October 1997, pp. 105-143

• Abstract: A sound and complete semantics is given for sequential, depth-first logic programming with a version of negation as failure. The semantics is logical in the sense that it is built up only from valuation functions (multi-valued logic interpretations in the style of Fitting and Kunen) and logically-motivated equivalence relations between formulas. The notion of predicate folding and unfolding with respect to a program (Tamaki, Sato, Levi et al.) and the universal notion of ``disjunctive unfolding'' (Andrews) are important elements of this semantics.

  The negation used is the version which returns an error indication whenever it is invoked on a non-ground goal. It is theoretically interesting that this form of negation, along with the left-to-right processing of depth-first logic programming, can be characterized logically with four-valued interpretations over an extended alphabet of terms. The fourth truth value, $N$, can be read operationally as ``floundering on negation''. The extension of the alphabet provides the semantics with a logical analogue of free variables. This intriguing technique may open the door to the characterization of other forms of practical negation, or of other language features involving groundness conditions.

James Andrews, Veronica Dahl and Fred Popowich, "Characterizing Logic Grammars: A Substructural Logic Approach." Journal of Logic Programming, v. 26 no. 3, March 1996, pp. 233-283

• Abstract: A characterization of Static Discontinuity Grammars (SDGs), a logic grammar formalism due to Dahl, is given in this paper. A substructural logic sequent calculus proof system is given which is shown to be equivalent to SDGs for parsing problems, in the sense that a string of terminal symbols is accepted by a grammar if and only if the corresponding sequent is derivable in the calculus. One calculus is given for each of the two major interpretations of SDGs; the two calculi differ by only a small restriction in one rule. Since SDGs encompass other major grammar formalisms, including DCGs, the calculi serve to characterize those formalisms as well.

James H. Andrews, "Foundational Issues in Implementing Constraint Logic Programming Systems." Science of Computer Programming, v. 25 (1995), pp. 117-147

• Abstract: Implementations of Constraint Logic Programming (CLP) systems are often incomplete with respect to the theories they are intended to implement. This paper studies two issues that arise in dealing with these incomplete implementations. First, the notion of incomplete ``satisfiability function'' (the analogue of unification) is formally defined, and the question of which such functions are reasonable is studied. Second, techniques are given, based on the notion of satisfiability function, for formally (proof-theoretically) specifying an intended CLP theory or a characterizing an existing CLP system. Such proof-theoretic characterizations have applications in proving soundness and completeness results, and proving properties of programs. Notions from substructural logic and the notion of Henkinness of the theory are shown to be important here.