Logic-Based Program Synthesis and Transformation: 8th International Workshop, LOPSTR'98, Manchester, UK, June 15-19, 1998, Selected Papers (Lecture Notes in Computer Science, 1559)

✍ Scribed by Pierre Flener (editor)

• Publisher: Springer
• Year: 1999
• Tongue: English
• Leaves: 341
• Category: Library

✦ Synopsis

This book presents the thoroughly refereed post-workshop proceedings of the 8th International Workshop on Logic-Based Program Synthesis and Transformation, LOPSTR'98 held in Manchester, UK in June 1998. The 16 revised full papers presented were carefully reviewed and selected during three rounds of inspection from a total of initially 36 extended abstracts submitted. Also included are eight short papers. Among the topics covered are logic specification, mathematical program construction, logic programming, computational logics, inductive program synthesis, constraint logic programs, and mathematical foundations.

✦ Table of Contents

Logic-Based Program Synthesis and Transformation
Preface
Programme Committee
Reviewers
Sponsors
Table of Contents
Attempto Controlled English - Not Just Another Logic Specification Language
Introduction
From English to Attempto Controlled English
An Example
ACE in a Nutshell
From ACE to Discourse Representation Structures
Translation
Constraining Ambiguity
Semantics of ACE Specifications
Model-Theoretic Interpretation
Events and States
Deductions from Discourse Representation Structures
Theorem Prover for Discourse Representation Structures
Query Answering
Hypothetical Reasoning
Abductive Reasoning
Executing an ACE Specification
Domain Knowledge
Conclusions
Reference
A Step Towards a Methodology for Mercury Program Construction: A Declarative Semantics for Mercury
Introduction
Notation
Deville's Methodology for Mercury Program Construction
Introduction
Example of Deville's Methodology for Mercury
First Attempt: The Declarative Semantics D0
Introduction
The Universe of Values U
The Denotation of Terms and Goals in D0
The Denotation of Types
Models of Type Correct Programs
A Sample Model in D0 of PAS
Declarative Semantics D
The Denotation of Terms and Goals
Models of Type Correct Programs
A Model of the Program P' AS
Discussion
Acknowledgments
References
Pragmatics in the Synthesis of Logic Programs
Why Domain Specific Systems are Needed
Pragmatics at Individual Stages of Design
Parameterisable Components
Synthesis by Slices
Enhancement by Meta-Interpretation
The Need for Integration Across Lifecycles
Language
Refinement Operations
Domain-Specific Example
Domain-Specific Refinements
Conclusions
References
Using Decision Procedures to Accelerate
Introduction
Separated Inference Rules
Procedures for Testing Satisfiability
Deductive Synthesis Decision Procedures
Amphion/NAIF Decision Procedures
A Procedure for Time Conversion
A Proof Using the Time Conversion Procedure
Implementation
Conclusion
REFERENCES
Synthesis of Programs in Abstract Data Types
Introduction
ADT specifications
Specifications
Active Proof Patterns and synthesis rules
Induction Principles
The Tail Recursion Principle
Descending Chain Principle
Conclusions and future works
References
Dischargeable sets
OOD Frameworks in Component-Based Software - Development in Computational Logic
Introduction
Overview of Our Approach to Program Development
Specification Frameworks
Closed Frameworks
Open Frameworks
Classes and Objects
ADT-frameworks
OBJ-frameworks
OOD Frameworks
Systems of Objects
Composite Objects
Conclusion
References
The Use of Renaming in Composing General Programs
Introduction and Motivations
General Program Expressions
Reusing Components
Information Hiding
Semantics
Concluding Remarks
References
Inductive Synthesis of Logic Programs by Composition of Combinatory Program Schemes
Introduction
Compositional Logic Programming
Combinators for Logic Programs
Semantics for Combinators
Recursion Combinators
Synthesizing Combinatory Logic Programs
Outline of the {sc CombInduce} Synthesizer
The {sc CombInduce} Synthesizer as a Metalogic Program
Synthesis with the {it Fold/} Combinators
Synthesis Involving the And Combinator
Synthesis with Would-be Appeal to Predicate Invention
Conclusions
References
Specialising Logic Programs with Respect to Call/Post Specifications
Introduction
Preliminaries
Programs and Derivations
Interpretations
Specialised Derivations and their Semantics
Specialised Derivations
Specialised Top-down Semantics
Specialised Fixpoint Semantics
Specialising Programs wrt Call/Post Specification
Specialised Partially Correct Programs
Specialised Programs
Equivalence of the Top-down and Fixpoint Semantics
Verifying Specialised Partial Correctness
An Example
References
Generalization in Hierarchies of Online Program Specialization Systems
Introduction
S-Graph-$n$
Syntax
Semantics
Meta-Programming Concepts
Metacoding
Hierarchy of Metacoded Values
Metavariables and their Domain
Configuration Values
Generalization of Configuration Values
Elevation and Generalization
Most Specific Domain Index
Most Specific Generalization
Embedding of Configuration Values
Self-Applicable Specialization
Related Work
Conclusion
References
Improving Homeomorphic Embedding for Online Termination
Introduction
Well-quasi orders and homeomorphic embedding
Comparing wbr's and wfo's
Nearly-Foundedness and Over-Eagerness
A more refined treatment of variables
Extended homeomorphic embedding
Discussion and Conclusion
Successes in Logic Programs
Introduction
Basic Notions
Successful Predicates
How to Verify that a Program is Successful
Accepted input types
Exhaustiveness of tests
Input-normalization
Input-subsumption
Analysis strategy
Applications
Conclusion
References
Appendix
Inferring and Compiling Termination for Constraint Logic Programs
Introduction
Preliminaries
CLP($chi $)
From CLP($chi $) to CLP($@mathcal {B}ool$)
Inferring left-termination conditions: The previous approach
Inferring extended left-termination conditions
Reordering to left-terminate
Conclusion
References
Strictness Analysis as Finite-Domain Constraint Solving
Introduction
Strictness Analysis
Wadler's Method for Lists
A Constraint-Based Method
The Translation
Other Data Types
Conclusion
References
Invariant Discovery via Failed Proof Attempts
Introduction
Background
Proof Planning
The Ripple Heuristic
Summary
A Proof Plan for Verification
Analysis of Failure
Replacement of Constants
Strengthening invariants
Refining Invariants
Results and Implementation
Related Work
Future Work
Conclusion
References
Preventing Instantiation Errors and Loops for Logic Programs with Multiple Modes Using block Declarations
Introduction
Preliminaries
Permutations and Modes
Permutation Nicely Moded Programs
Permutation Well Typed Programs
Permutation Simply Typed Programs
Errors Related to Built-ins
The Connection between Delay Declarations and Type Errors
Exploiting Constant Types
Atomic Positions
Termination
Termination by not Using Speculative Bindings
Termination by not Making Speculative Bindings
Related Work
Conclusion and Future Work
References
Algorithms for Synthesizing Reactive Systems: A Perspective
Schema-Guided Synthesis of CLP Programs*
Introduction and Specifications
A Global Search Program Schema for CLP
Schema Particularisations and the Synthesis Method
Conclusion
References
Abstract:Proof Planning with Program Schemas
Introduction
Proof Planning
The Relationship of Schemas to Proof Planning
Augmenting Schemas with a Heuristic Component
Conclusions
References
Logical Synthesis of Imperative O.O. Programs
Mathematical Foundations for Program Transformations
Program Transformations: An Emerging Paradigm
A Calculus of Programming by Parts
Software Incrementation
Software Merging
Software Adaptation
Software Composition
Conclusion
References
An Exhaustive-Search Method Using Layered Streams Obtained Through a Meta-Interpreter for Chain Programs
Introduction
Layered streams
An exhaustive-search meta-interpreter for chain programs
Chain programs
An exhaustive-search meta-interpreter
Beyond chain form
References
Bottom-Up Specialisation of Logic Programs
Introduction and Motivation
A Framework for Bottom-up Specialisation
References
Myrtle: A Set-Oriented Meta-Interpreter Driven by a "Relational" Trace for Deductive Databases Debugging
Introduction
Debugging tools for deductive database systems
Driving a meta-interpreter with a trace
Conclusion
References
Author Index