Reasoning about multiple related abstractions with MultiStar
| Autor: | Stephan van Staden, Cristiano Calcagno |
|---|---|
| Rok vydání: | 2010 |
| Předmět: |
Class (computer programming)
Iterator Object-oriented programming Theoretical computer science Computer science Programming language Multiple inheritance Predicate (mathematical logic) Separation logic computer.software_genre Computer Graphics and Computer-Aided Design Boolean algebra symbols.namesake Inheritance (object-oriented programming) Data processing computer science Logical programming symbols ddc:004 computer Axiom Software |
| Zdroj: | OOPSLA Technical Report / ETH Zurich, Department of Computer Science, 666 |
| ISSN: | 1558-1160 0362-1340 |
| DOI: | 10.1145/1932682.1869501 |
| Popis: | Encapsulated abstractions are fundamental in object-oriented programming. A single class may employ multiple abstractions to achieve its purpose. Such abstractions are often related and combined in disciplined ways. This paper explores ways to express, verify and rely on logical relationships between abstractions. It introduces two general specification mechanisms: export clauses for relating abstractions in individual classes, and axiom clauses for relating abstractions in a class and all its descendants. MultiStar, an automatic verification tool based on separation logic and abstract predicate families, implements these mechanisms in a multiple inheritance setting. Several verified examples illustrate MultiStar's underlying logic. To demonstrate the flexibility of our approach, we also used MultiStar to verify the core iterator hierarchy of a popular data structure library. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|