Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

Hoare logic can be used for proving program correctness (e.g. for deriving correctness statements for the whole program from the statements for the individual commands or constructions; good summary is http://www.cis.upenn.edu/~bcpierce/sf/Hoare.html). The question is - is there any line of research where Hoare-style reasoning can be made for programs that creates and deletes objects.

One thought can be that this reasoning can be simulated by defining large pool of objects which have (for the purposes of correctness analysis) additional state attribute with values from the enumeration {not-created, created, destroyed}. But I guess that better approach should exist.

Are there any references or keywords for furher search into this matter.

share|improve this question
add comment

3 Answers 3

There is a lot of work on Hoare Logic for object oriented programs, and for reasoning about memory allocation and deallocation. Some starting points:

  1. A Syntax-Directed Hoare Logic for Object-Oriented Programming Concepts
  2. Separation Logic, does not target OO-languages specifically but applies to the more fundamental problem of reasoning about heap-allocated data.
  3. jStar: Bringing separation logic to Java
share|improve this answer
add comment

Vijay D has mentioned both separation logic and jStar, which is a tool for verifying Java programs.

jStar uses the logic Matthew Parkinson developed in his PhD thesis, Local Reasoning for Java, which gives a separation-based Hoare logic for verifying Java programs. It is a very well written thesis, and offers one of the most readable introductions to modern techniques for verifying imperative/OO programs.

My own thesis is less well-written, but it shows how to extend this style of separation logic to a full Reynolds-style specification logic, which makes it easier to specify and prove correct higher-order imperative programs, such as those using callbacks. This is not for Java, though, but rather for an ML or Haskell-like language.

share|improve this answer
add comment

If you are interested in prototype-based objects (such as the ones found in JavaScript), the paper "Towards a Program Logic for JavaScript" describes a separation logic for JavaScript programs. ACM link or direct PDF

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.