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 \setlog, 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 \setlog 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.
Adding partial functions to Constraint Logic Programming with sets / Cristiá, Maximiliano; Rossi, Gianfranco; Frydman, Claudia. - In: THEORY AND PRACTICE OF LOGIC PROGRAMMING. - ISSN 1471-0684. - 15:4-5(2015), pp. 651-665. [10.1017/S1471068415000290]
Adding partial functions to Constraint Logic Programming with sets
ROSSI, Gianfranco;
2015-01-01
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 \setlog, 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 \setlog 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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.