In this paper, we propose an efficient technique to statically manage integrity constaints in object-oriented database programming languages. We palce ourselves in the context of a ismplified database programming language, colse to O sub 2, in which we assume that updates are undertaken by means of mehods. An important issue when dealing with ocnstraints is that of efficiency. A naive managment of usch constraints can cause a severe floundering of the over-all system. Our basic assumption is that the run-time checking of constraints is too costly to be undertaken systmatically. Therefore, methods that are always safe with repsect to integrity constraints should be proven so at compile time. The run-time checks should only concern the remaining methods. To that purpose, we propose a new approach, based on the use of predicate transformaers ocmbined with automatic theorem proving techniques, to prove the invariance of integrity constraints under complex methods. We then describe the current implementatior, of our prototype, and report some experiments that have been eprformed with it on non trivial examples. The counterpart of the problem of program verification is that of program correction. Static analysis techniques can also be applied to solve that problem. We present a systematic apporach to undertake the automatic ocrrection of potentialy unsafe methods. However, the advantages of the latter techniqeu are not as clear as those of porgram verification. We will therefore discuss some arguments for and against the use of metod correction.
展开▼
机译：在本文中，我们提出了一种有效的技术来静态管理面向对象的数据库编程语言中的完整性约束。我们将自己放在一种简化的数据库编程语言的上下文中，紧贴O sub 2，在该语言中我们假定更新是通过方法进行的。处理障碍时，一个重要的问题是效率。幼稚的管理限制条件会导致整个系统严重混乱。我们的基本假设是约束的运行时检查成本太高，无法系统地进行。因此，应该证明对完整性约束始终是安全的方法，以便在编译时使用。运行时检查应仅涉及其余方法。为此，我们提出了一种新方法，该方法基于谓词变换与自动定理证明技术结合使用，以证明复杂方法下完整性约束的不变性。然后，我们描述原型的当前实现方式，并报告在非平凡示例中进行的一些实验。与程序验证问题相对应的是程序校正问题。静态分析技术也可以用于解决该问题。我们提出了一种系统的方法来进行潜在不安全方法的自动掩盖。但是，后一种技术的优势并不像porgram验证那样明显。因此，我们将讨论支持和反对使用方法校正的一些论点。
展开▼
