Constraint-logic object-oriented programming, for example using Muli, facilitates the integrated development of business software that occasionally involves finding solutions to constraint-logic problems. The availability of object-oriented features calls for the option to use objects as logic variables as well, as opposed to being limited to primitive type logic variables. The present work contributes a concept for reference type logic variables in constraint-logic object-oriented programming that takes arbitrary class hierarchies of programs written in object-oriented languages into account. The concept discusses interactions between constraint-logic object-oriented programs and reference type logic variables, particularly invocations on and access to logic variables, type operations, and equality. Furthermore, it proposes approaches as to how these interactions can be handled by a corresponding execution environment.
The type unification algorithm presented by @cite_5 can be used for Java type inference. Although their work emanates from a different standpoint, the type unification could be re-used for formulating the subtype relations for the constraints in this work.
@cite_5
1872053036
With the introduction of Java 5.0 the type system has been extended by parameterized types, type variables, type terms, and wildcards. As a result very complex types can arise. The term @math is for example a correct type in Java 5.0. In this paper we present a type unification algorithm for Java 5.0 type terms. The algorithm unifies type terms, which are in subtype relationship. For this we define Java 5.0 type terms and its subtyping relation, formally. As Java 5.0 allows wildcards as instances of generic types, the subtyping ordering contains infinite chains. We show that the type unification is still finitary. We give a type unification algorithm, which calculates the finite set of general unifiers.