LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:exercises_05 [2008/03/25 14:00]
piskac
sav08:exercises_05 [2008/03/25 14:02]
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+