Modular verification of OO programs with interfaces | |
Qiu, Zongyan ; Hong, Ali ; Liu, Yijing | |
2012 | |
英文摘要 | Interface types in OO languages support polymorphism, abstraction and information hiding by separating interfaces from their implementations. The separation enhances modularity of programs, however, it causes also challenges to the formal verification. Here we present a study on interface types, and develop a specification and verification theory based on our former veriJ framework. We support multi-specifications for classes inherited from interfaces and the superclass, and keep the verification modularly without re-touching the verified code. The concepts developed in veriJ, namely the abstract specification and specification predicate, play important roles in this extension, and thus are proved widely useful and very natural in the formal proofs of OO programs. ? 2012 Springer-Verlag.; EI; 0 |
语种 | 英语 |
出处 | EI |
内容类型 | 其他 |
源URL | [http://hdl.handle.net/20.500.11897/411929] ![]() |
专题 | 数学科学学院 |
推荐引用方式 GB/T 7714 | Qiu, Zongyan,Hong, Ali,Liu, Yijing. Modular verification of OO programs with interfaces. 2012-01-01. |
个性服务 |
查看访问统计 |
相关权益政策 |
暂无数据 |
收藏/分享 |
除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。
修改评论