Formal Verification of `Programming to Interfaces' Programs
    Download PDF
Jianhua Zhao,Xuandong Li. Formal Verification of `Programming to Interfaces' Programs. International Journal of Software and Informatics, 2016,10(4):0
Hits: 1910
Download times: 1179
Abstract:This paper presents a formal approach to specify and verify object-oriented programs written in the `programming to interfaces' paradigm. In this approach, besides the methods to be invoked by its clients, an interface also declares a set of abstract and polymorphic function/predicate symbols, together with a set of constraints about these symbols. The methods declared in this interface are specified using these abstract symbols. A class implementing this interface can give its own definitions to the abstract symbols, as long as all the constraints are satisfied. This class implements all the methods declared in the interface such that the method specification declared in the interface are satisfied w.r.t. the function symbol definitions in this class. Based on the constraints about the abstract symbols, client code using the interfaces can be specified and verified precisely without knowing what classes implement the interfaces. Given more information about the implementing classes, the specifications of the client code can be specialized into more precise ones without re-verifying the client code.
keywords:code verification  object oriented  interface  polymorphism
View Full Text  View/Add Comment  Download reader



Top Paper  |  E-mail Alert  |  Publication Ethics  |  New Version

© Copyright by Institute of Software, the Chinese Academy of Sciences

京公网安备 11040202500065号