|
Abstract : |
Abstract. This paper describes a way of modeling inheritance (in objectoriented programming languages) in higher order logic. This particular approach is used in the loop project for reasoning about java classes, with the proof tools pvs and isabelle. It relies on nested interface types to capture the superclasses, elds, methods, and constructors of classes, together with suitable casting functions incorporating the dierence between hiding of elds and overriding of methods. This leads to the proper handling of late binding, as illustrated in several verication examples. 1, |
