this book constitutes the refereed proceedings of the 10thinternational Symposium on programming Languages, Implementations, Logics, and Programs, PLILP'98, held jointly withthe 6thinternationalconference on A...
详细信息
ISBN:
(数字)9783540497660
ISBN:
(纸本)9783540650126
this book constitutes the refereed proceedings of the 10thinternational Symposium on programming Languages, Implementations, Logics, and Programs, PLILP'98, held jointly withthe 6thinternationalconference on Algebraic and Logic programming, ALP'98, in Pisa, Italy, in September 1998.;the 26 revised full papers presented were carefully reviewed and selected from a total of 68 submissions. Also included are two invited papers and abstracts of two tutorials. the papers are organized in topical sections on verification, logic programming, static analysis, software methodologies, object oriented programming, term rewriting, functional programming, metaprogramming, optimal evaluation, integration, and constraint solving.
Diagrammatic human-computer interfaces are now becoming standard. In the near future, diagrammatic front-ends, such as those of UML-based CASE tools, will be required to offer a much more intelligent behavior than jus...
详细信息
ISBN:
(纸本)3540666265
Diagrammatic human-computer interfaces are now becoming standard. In the near future, diagrammatic front-ends, such as those of UML-based CASE tools, will be required to offer a much more intelligent behavior than just editing. Yet there is very little formal support and there are almost no tools available for the construction of such environments. the present paper introduces a constraint-based formalism for the specification and implementation of complex diagrammatic environments. We start from grammar-based definitions of diagrammatic languages and show how a constraint solver for diagram recognition and interpretation can automatically be constructed from such grammars. In a second step, the capabilities of these solvers are extended by allowing to axiomatise formal diagrammatic systems, such as Venn Diagrams, so that they can be regarded as a new constraint domain. the ultimate aim of this schema is to establish a language of type CLP(Diagram) for diagrammatic reasoning applications.
Many combinatorial problems encountered in practice involve constraints that require that a, set of variables take distinct or equal values. the ALLDIFFERENT constraint, in particular, ensures that;all variables take ...
详细信息
ISBN:
(纸本)9783642042430
Many combinatorial problems encountered in practice involve constraints that require that a, set of variables take distinct or equal values. the ALLDIFFERENT constraint, in particular, ensures that;all variables take distinct values. Two soft variants of this constraint were proposed ill [4];defined either with respect to a so-called variable or graph-based cost function. When requiring similarity, as' opposed to diversity, one can consider the dual definition either for the cost;or for the basic constraint, itself, that is, ALLEQUAL in our case. Six cost, functions call be defined by exploring every combination of these definitions. It is therefore natural to study the complexity of achieving arc consistency and bounds consistency oil them. From our earlier work oil this topic all open problem remained, namely achieving bounds Consistency oil the maximisation of the SOFTALLDIFF constraint when considering the graph-based cost. In this paper we resolve this problem. therefore. we give a complete taxonomy of constraints of equality and difference, based oil the alternative objective functions used for the soft, variants.
the constraint satisfaction problem is in general NP-hard. As such, our aim is to identify tractable classes of constraint satisfaction problem instances (CSPs). Tractable classes of CSPs are normally described by lim...
详细信息
ISBN:
(纸本)3540462678
the constraint satisfaction problem is in general NP-hard. As such, our aim is to identify tractable classes of constraint satisfaction problem instances (CSPs). Tractable classes of CSPs are normally described by limiting either the structure or the language of the CSPs. Structural decomposition methods identify CSPs whose reduction to the acyclic class is bound by a polynomial. these structural decompositions have been a very useful way to identify large tractable classes. However, these decomposition techniques have not yet been applied to relational tractability results. In this paper we introduce the notion of a typed guarded decomposition as a way to generalize the structural decompositions. We develop a no-promise algorithm which derives large new tractable classes of CSPs that are not describable as purely structural nor purely relational classes.
this paper presents a novel domain-consistency algorithm which does not maintain supports dynamically during propagation, but rather maintain forbidden values. It introduces the optimal NAC4 (negative AC4) algorithm b...
详细信息
ISBN:
(纸本)9783642153952
this paper presents a novel domain-consistency algorithm which does not maintain supports dynamically during propagation, but rather maintain forbidden values. It introduces the optimal NAC4 (negative AC4) algorithm based on this idea. It further shows that maintaining forbidden values dynamically allows the generic algorithm AC5 to achieve domain consistency in time O(ed) for classes of constraints in which the number of supports is O(d(2)) but the number of forbidden values is O(d). the paper also shows how forbidden values and supports can be used jointly to achieve domain consistency on logical combinations of constraints and to compute validity as well as entailment of constraints. Experimental results show the benefits of the joint exploitation of supports and forbidden values.
作者：
Golden, KPang, WLNASA
Ames Res Ctr Computat Sci Div Moffett Field CA 94035 USA NASA
Ames Res Ctr QSS Grp Inc Moffett Field CA 94035 USA
this paper discusses an approach to representing and reasoning about constraints over strings. We discuss how string domains can often be concisely represented using regular languages, and how constraints over strings...
详细信息
ISBN:
(纸本)3540202021
this paper discusses an approach to representing and reasoning about constraints over strings. We discuss how string domains can often be concisely represented using regular languages, and how constraints over strings, and domain operations on sets of strings, can be carried out using this representation.
the proceedings contain 19 papers. the topics discussed include: the JavaFest: a collaborative learning technique for Java programming courses;an experimental environment for teaching Java security;patterns and tracea...
ISBN:
(纸本)9781605582238
the proceedings contain 19 papers. the topics discussed include: the JavaFest: a collaborative learning technique for Java programming courses;an experimental environment for teaching Java security;patterns and traceability in teaching software architecture;a framework for command processing in Java/Swing programs based on the MVC pattern;the PIM: an innovative robot coordination model based on Java thread migration;self-configuring object-to-relational mapping queries;portable execution of legacy binaries on the Java virtual machine;a lazy developer approach: building a JVM withthird party software;speculative improvements to verifiable bounds check elimination;constraint based optimization of stationary fields;optimized strings for Java HotSpot™ virtual machine;and SlimVM: optimistic partial program loading for connected embedded Java virtual machines.
this paper introduces a constraint language H for finite partial maps (a.k.a. heaps) that incorporates the notion of separation from Separation Logic. We use H to build an extension of Hoare Logic for reasoning over h...
详细信息
ISBN:
(纸本)9783642406263;9783642406270
this paper introduces a constraint language H for finite partial maps (a.k.a. heaps) that incorporates the notion of separation from Separation Logic. We use H to build an extension of Hoare Logic for reasoning over heap manipulating programs using (constraint-based) symbolic execution. We present a sound and complete algorithm for solving quantifier-free (QF) H-formulae based on heap element propagation. An implementation of the H-solver has been integrated into a Satisfiability Modulo theories (SMT) framework. We experimentally evaluate the implementation against Verification Conditions (VCs) generated from symbolic execution of large (heap manipulating) programs. In particular, we mitigate the path explosion problem using subsumption via interpolation - made possible by the constraint-based encoding.
Forbidden patterns problems are a generalisation of (finite) constraint satisfaction problems which are definable in Feder and Vardi's logic MMSNP [1]. in fact, they are examples of infinite constraint satisfactio...
详细信息
ISBN:
(纸本)9783642153952
Forbidden patterns problems are a generalisation of (finite) constraint satisfaction problems which are definable in Feder and Vardi's logic MMSNP [1]. in fact, they are examples of infinite constraint satisfaction problems with nice model theoretic properties introduced by Bodirsky [2]. In previous work [3], we introduced a normal form for these forbidden patterns problems which allowed us to provide an effective characterisation of when a problem is a finite or infinite constraint satisfaction problem. One of the central concepts of this normal form is that of a recolouring. In the presence of a recolouring from a forbidden patterns problem Omega(1) to another forbidden patterns problem Omega(2), containment of Omega(1) in Omega(2) follows. the converse does not hold in general and it remained open whether it did in the case of problems being given in our normal form. In this paper, we prove that this is indeed the case. We also show that the recolouring problem is Pi(p)(2)-harpd and in Sigma(p)(3).
暂无评论