Development of Transformation Functions Assisted by a Theorem Prover
作者： Pascal Molli , Michaël Rusinowitch , Gérald Oster , Imine Abdessamad
DOI:
关键词:
摘要: Transformational approach requires to write transformation functions that ensure properties C1 and C2. Proving these conditions on complex typed objects is a serious bottleneck for the application of this approach. We propose use theorem prover assist development safe functions. In paper, we present how have designed in way set an XML object.
参考文章(10)
Pascal Molli, Abdelmajid Bouazza, Unifying coupled and uncoupled collaborative work in virtual teams conference on computer supported cooperative work. ,(2000)
P. Molli, H. Skaf-Molli, G. Oster, S. Jourdain, SAMS: synchronous, asynchronous, multi-synchronous environments computer supported cooperative work in design. pp. 80- 84 ,(2002) , 10.1109/CSCWD.2002.1047653
M. Suleiman, M. Cart, J. Ferrie, Concurrent operations in a distributed and mobile collaborative environment international conference on data engineering. pp. 36- 45 ,(1998) , 10.1109/ICDE.1998.655755
Peter Padawitz, Swinging types = functions + relations + transition systems Theoretical Computer Science. ,vol. 243, pp. 93- 165 ,(2000) , 10.1016/S0304-3975(00)00171-7
Chengzheng Sun, David Chen, Consistency maintenance in real-time collaborative graphics editing systems ACM Transactions on Computer-Human Interaction. ,vol. 9, pp. 1- 41 ,(2002) , 10.1145/505151.505152
Adel Bouhoula, Micha�l Rusinowitch, Implicit induction in conditional theories Journal of Automated Reasoning. ,vol. 14, pp. 189- 235 ,(1995) , 10.1007/BF00881856
Matthias Ressel, Doris Nitsche-Ruhland, Rul Gunzenhäuser, An integrating, transformation-oriented approach to concurrency control and undo in group editors conference on computer supported cooperative work. pp. 288- 297 ,(1996) , 10.1145/240080.240305
Nicolas Vidot, Michelle Cart, Jean Ferrié, Maher Suleiman, Copies convergence in a distributed real-time collaborative environment conference on computer supported cooperative work. pp. 171- 180 ,(2000) , 10.1145/358916.358988
C. A. Ellis, S. J. Gibbs, Concurrency control in groupware systems international conference on management of data. ,vol. 18, pp. 399- 407 ,(1989) , 10.1145/66926.66963
Chengzheng Sun, Xiaohua Jia, Yanchun Zhang, Yun Yang, David Chen, Achieving convergence, causality preservation, and intention preservation in real-time cooperative editing systems ACM Transactions on Computer-Human Interaction. ,vol. 5, pp. 63- 108 ,(1998) , 10.1145/274444.274447