A liquid type is an ordinary Hindley-Milner type annotated with a logical predicate that states the properties satisfied by the elements of that type. Liquid types are a powerful tool for program verification, as programmers can use them to specify pre- and post conditions of their programs, whereas the predicates of intermediate variables and auxiliary functions are inferred automatically. Type inference is feasible in this context, as the logical predicates within liquid types are constrained to a quantifier-free logic to maintain decidability. In this article, we extend liquid types by allowing them to contain quantified properties on arrays so that they can be used to infer invariants on array-related programs (e.g., implementations of sorting algorithms). Although quantified logic is, in general, undecidable, we restrict properties on arrays to a decidable subset introduced by Bradley et al. We describe in detail the extended type system, the verification condition generator, and the iterative weakening algorithm for inferring invariants. After proving the correctness and completeness of these two algorithms, we apply them to find invariants on a set of algorithms involving array manipulations.

This work is aimed to show a concrete implementation of a deductive database system based on the scheme HH_(C) (Hereditary Harrop Formulas with Negation and Constraints) following a fixpoint semantics proposed in a previous work. We have developed a Prolog implementation for this scheme that is constraint system independent, therefore allowing to use it as a base for any instance of the formal scheme. We have developed several specific constraint systems: Real numbers, integers, Boolean and user-defined enumerated types. We have added types to the database so that relations become typed (as tables in relational databases) and each constraint is mapped to its corresponding constraint system. The predicates that compute the fixpoint giving the meaning to a database are described. In particular, we show the implementation of a forcing relation (for derivation steps) and highlight how the inherent difficulties have been overcome in a system allowing hypothetical queries, which make the database dynamically grow.

This paper is focused on a double extension of traditional Logic Programming which enhances it following two different approaches. On one hand, extending Horn logic to hereditary Harrop formulas HH), in order to improve the expressive power; on the other, incorporating constraints, in order to increase the efficiency. For this combination, called HH(C), an operational semantics exists, but no declarative semantic for it has been defined so far.One of the main features of (Constraint) Logic Programming is that the algorithmic behavior of (constraint) logic programs and its mathematical interpretations agree with each other, in the sense that the declarative meaning of a program can be interpreted operationally as a goal-oriented search for solutions. Both operational (algorithmic) and declarative (mathematical) semantics for programs are useful and widely developed in the frame of Logic Programming as well as in its extension, Constraint Logic Programming.For these reasons, HH(C) was in need of a more mathematical interpretation of programs. In this paper some fixed point semantics for HH(C) are presented. Taking as a starting point the techniques used by Miller to interpret the fragment of HH that incorporates intuitionistic implication in goals, we have formulated two novel extensions capable of dealing with the whole HH logic, including universal quantifiers, as well as with the presence of constraints. Those semantics are proved to be sound and complete w.r.t. the operational semantics of HH(C).

Constraint Logic Programming (CLP) and Hereditary Harrop formulas (HH) are two well known ways to enhance the expressivity of Horn clauses. In this paper, we present a novel combination of these two approaches. We show how to enrich the syntax and proof theory of HH with the help of a given constraint system, in such a way that the key property of HH as a logic programming language (namely, the existence of uniform proofs) is preserved. We also present a procedure for goal solving, showing its soundness and completeness for computing answer constraints. As a consequence of this result, we obtain a new strong completeness theorem for CLP that avoids the need to build disjunctions of computed answers, as well as a more abstract formulation of a known completeness theorem for HH.