Algebraic reasoning for object-oriented programming
Algebraic reasoning for object-oriented programming
复制标题
面向对象编程的代数推理
DOI：
10.1016/j.scico.2004.03.003
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
Márcio Cornélio
中科院分区：
文献类型：
--
作者：
Paulo Borba;A. Sampaio;Ana Cavalcanti;Márcio Cornélio
我们提出了一种类似于顺序Java子集的语言的代数定律，它包括继承、递归类、动态绑定、访问控制、类型测试和强制类型转换、赋值，但没有共享。这些定律在最弱前提语义方面被证明是正确的。我们还证明了它们是完备的，因为它们足以将任意规划化为实质上接近于命令式规划的范式；如果我们的语言具有递归记录，则可以进一步消除剩余的面向对象结构。这表明我们的定律具有足够的表达能力，可以正式推导出保持行为的程序转换；我们通过推导可证明正确的重构来说明这一点。
We present algebraic laws for a language similar to a subset of sequential Java that includes inheritance, recursive classes, dynamic binding, access control, type tests and casts, assignment, but no sharing. These laws are proved sound with respect to a weakest precondition semantics. We also show that they are complete in the sense that they are sufficient to reduce an arbitrary program to a normal form substantially close to an imperative program; the remaining object-oriented constructs could be further eliminated if our language had recursive records. This suggests that our laws are expressive enough to formally derive behaviour preserving program transformations; we illustrate that through the derivation of provably-correct refactorings.