Proving Correctness of Transformation Functions in Real-Time Groupware
Proving Correctness of Transformation Functions in Real-Time Groupware
复制标题
证明实时组件中转换函数的正确性
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
M. Rusinowitch
中科院分区：
文献类型：
--
作者：
Abdessamad Imine;P. Molli;G. Oster;M. Rusinowitch
操作转换是一种允许构建实时群件工具的方法。这种方法需要正确的转换函数。证明这些变换函数的正确性是非常复杂和容易出错的。在本文中，我们将展示如何定理证明可以解决这个严重的瓶颈。为了验证我们的方法，我们已经验证了在字符串上定义的最先进的转换函数的正确性，并得到了令人惊讶的结果。定理证明器提供的反例帮助我们为字符串定义了新的正确的变换函数。
Operational transformation is an approach which allows to build real-time groupware tools. This approach requires correct transformation functions. Proving the correction of these transformation functions is very complex and error prone. In this paper, we show how a theorem prover can address this serious bottleneck. To validate our approach, we have verified the correctness of state-of-art transformation functions defined on Strings with surprising results. Counter-examples provided by the theorem prover have helped us to define new correct transformation functions for Strings.