Adding Partial Functions to Constraint Logic Programming with Sets

TL;DR

This paper introduces partial functions as a primitive feature in the {log} constraint logic programming language, enhancing its ability to handle set-theoretic formulas from formal specifications like Z, with empirical evaluation of efficiency.

Contribution

It extends {log} with partial functions as first-class citizens, improving flexibility and generality in set-theoretic reasoning within the language.

Findings

Extended {log} constraint solver to support partial functions.

Empirical assessment shows improved handling of Z specifications.

Demonstrated efficiency in solving non-trivial set-theoretical goals.

Abstract

Partial functions are common abstractions in formal specification notations such as Z, B and Alloy. Conversely, executable programming languages usually provide little or no support for them. In this paper we propose to add partial functions as a primitive feature to a Constraint Logic Programming (CLP) language, namely {log}. Although partial functions could be programmed on top of {log}, providing them as first-class citizens adds valuable flexibility and generality to the form of set-theoretic formulas that the language can safely deal with. In particular, the paper shows how the {log} constraint solver is naturally extended in order to accommodate for the new primitive constraints dealing with partial functions. Efficiency of the new version is empirically assessed by running a number of non-trivial set-theoretical goals involving partial functions, obtained from specifications written in Z.