{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.
翻译：{log} (读“ setlog” ) 是一种约束逻辑编程语言( CLP) 语言和可引用性解析器, 其限制领域是有限组数理论。 根于 CLP 和 Prolog, {log} 基本上提供了一种非类型语言。 因此, 它可以接受使解答器产生不想要的行为的公式。 此外, {log} 用户在程序上可能会犯错误, 而这种错误通常会被类型检查器所捕捉。 特别是, {log} 被提议为 B 和 Z 规格的原型语言, 它们是输入格式主义的。 然后, 没有 {log} 类型系统, 用户需要手动填补空白 。 因此, 在本文中, 我们定义了一种类型系统, 并为 {log} 设置了类型校验器 。 类型系统被证明是安全的( sound), 通过将类型安全性编程的功能性编程配方法适应于 CLPLP 上。 我们还展示了类型和 CLP 如何组合, 来为程序正确性提供更有力的保证 。 最后, 我们从类型系统、 类型校验器及其组合与域与 CLPLPO 到真实- 案例研究 。
相关内容
微信扫码咨询专知VIP会员