3
$\begingroup$

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.

Improve this question
$\endgroup$
10
$\begingroup$

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
Improve this answer
$\endgroup$
7
$\begingroup$

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.

Improve this answer
$\endgroup$
0
$\begingroup$

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

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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