Logic and Formal Methods

A Calculus for Data Abstraction

  • Links:PDF
  • When trying to prove program correctness, verifiers have to struggle with different problems, a major one being the frame problem: knowing, which parts of the program state (mainly encoded in the heap) change by a given action, or rather which parts do not. The question becomes even harder, when abstraction is involved, for example, in an object-oriented context, by inheritance. Specifications for parent classes should be able to cover the behaviour of child classes, too, without any knowledge about the latter ones. A promising approach, which has come up in the recent years, is data abstraction in combination with explicit dependencies: specification-only variables, functions or predicates, which do not directly correspond to any program data, are introduced (data abstraction) and it is possible to specify, what other data or actions have an influence on their values (explicit dependencies). This approach is considered for the KeY program verification tool, using dynamic logic. This thesis examines, to what extent the abstract specification functions (observers) and explicit dependencies can be exploited to simplify logical expressions on a syntactical level. A term rewriting system is used for that task, its possibilities and theoretical limits are analysed.


  author       = {Roman Krenick\'y},
  title        = {A Calculus for Data Abstraction},
  howpublished = {Diplomarbeit, Fakult{\"a}t f{\"u}r Informatik, Universit\"at Karlsruhe},
  year         = {2009}