A Typechecker for a Set-Based Constraint Logic Programming Language
share
log (read 'setlog') is a Constraint Logic Programming (CLP) language and satisfiability solver whose constraint domain is the theory of finite sets. Rooted in CLP and Prolog, log essentially provides an untyped language. As such it can accept formulas that make the solver to produce unwanted behaviors. Besides, log users may make mistakes in their programs that would normally be caught by a typechecker. In particular, log has been proposed as a prototyping language for B and Z specifications, which are typed formalisms. Then, without a type system for log there is a gap that users need to fill manually. Therefore, in this paper we define a type system and implement a typechecker for log. The type system is proved to be safe (sound) by adapting the functional programming formulation of type safety to the CLP context. We also show how types and CLP can be combined to provide stronger assurances on program correctness. Finally, we apply the type system, the typechecker and their combination with CLP to a real-world case study from the aeronautic domain.
READ FULL TEXT