A Liskov Principle for Delta-Oriented Programming
A Liskov Principle for Delta-Oriented Programming
复制标题
面向 Delta 编程的 Liskov 原理
DOI：
10.1007/978-3-642-34026-0_4
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Ina Schaefer
中科院分区：
文献类型：
--
作者：
Reiner Hähnle;Ina Schaefer
在对软件产品家族的正式验证中，一个不仅可以分析程序，而且还必须对被重复使用以获取软件产品的工件和组件作用。由于产品的数量在伪影的数量中是指数级的，因此以模块化的方式进行验证至关重要。当代码重用基于OO编程中的类继承时，Liskov的原理是实现模块化验证的标准设备。但是，软件系列采用了与继承相比，采用其他可变性建模技术。面向Delta的编程是一种实施程序家族的方法，通过核心程序的逐步转换来实现代码重复使用。我们为面向三角洲的编程定义了Liskov原理，并表明它可以实现该范式中开发的软件家族的模块化验证。
In formal verification of software product families one not only analyses programs, but must act on the artifacts and components which are reused to obtain software products. As the number of products is exponential in the number of artifacts, it is crucial to perform verification in a modular way. When code reuse is based on class inheritance in OO programming, Liskov's principle is a standard device to achieve modular verification. Software families, however, employ other variability modeling techniques than inheritance. Delta-oriented programming is an approach to implement a family of programs where code reuse is achieved via gradual transformation of a core program. We define a Liskov principle for delta-oriented programming and show that it achieves modular verification of software families developed in that paradigm.