| 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: 2004 |
| Download times: 1282 |
|
|
| 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 |
|
|
|
