Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:exercises_05 [2008/03/25 13:59] piskac |
sav08:exercises_05 [2008/03/25 14:02] (current) piskac |
||
---|---|---|---|
Line 5: | Line 5: | ||
Abstract: | Abstract: | ||
- | Conventional specifications for object-oriented (OO) programs must adhere to behavioral subtyping in support of class inheritance and method overriding. However, this requirement inherently weakens the specifications of overridden methods in superclasses, leading to imprecision during program reasoning. To address this, we advocate a fresh approach to OO verification that focuses on the distinction and relation between specifications that cater to calls with static dispatching from those for calls with dynamic dispatching. We formulate a novel specification subsumption that can avoid code re-verification, where possible. | + | Conventional specifications for object-oriented (OO) programs |
- | + | must adhere to behavioral subtyping in support of class inheritance | |
- | Using a predicate mechanism, we propose a flexible scheme for supporting class invariant and lossless casting. Our aim is to lay the foundation for a practical verification system that is precise, concise and modular for sequential OO programs. We exploit the separation logic formalism to achieve this. | + | and method overriding. However, this requirement inherently |
+ | weakens the specifications of overridden methods in superclasses, | ||
+ | leading to imprecision during program reasoning. To address this, | ||
+ | we advocate a fresh approach to OO verification that focuses | ||
+ | on the distinction and relation between specifications that | ||
+ | cater to calls with static dispatching from those for calls with | ||
+ | dynamic dispatching. We formulate a novel specification subsumption | ||
+ | that can avoid code re-verification, where possible. | ||
+ | |||
+ | Using a predicate mechanism, we propose a flexible scheme for | ||
+ | supporting class invariant and lossless casting. Our aim is to lay | ||
+ | the foundation for a practical verification system that is precise, | ||
+ | concise and modular for sequential OO programs. We exploit the separation | ||
+ | logic formalism to achieve this. | ||
Line 15: | Line 28: | ||
* Semantic proof of drinker's paradox | * Semantic proof of drinker's paradox | ||
- | * Monotonicity of semantic consequence | + | |
- | * Sets of sentences with only finite and with only infinite models | + | |
- | * Herbrand universe | + | |
- | * Resolution proofs | + | |