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

<ol>
<li><a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.2984" rel="nofollow">A Syntax-Directed Hoare Logic for Object-Oriented Programming Concepts</a></li>
<li><a href="http://en.wikipedia.org/wiki/Separation_logic" rel="nofollow">Separation Logic</a>, does not target OO-languages specifically but applies to the more fundamental problem of reasoning about heap-allocated data.</li>
<li><a href="http://www.jstarverifier.org/" rel="nofollow">jStar: Bringing separation logic to Java</a></li>
</ol>

CC BY-SA 3.0
2012-12-25T03:12:28.033Z
2013-01-03T17:55:20.963Z
2013-01-03T17:55:20.963Z
Vijay D
<p>Vijay D has mentioned both separation logic and jStar, which is a tool for verifying Java programs. </p>

<p>jStar uses the logic Matthew Parkinson developed in his PhD thesis, <a href="http://www.cl.cam.ac.uk/~mjp41/Thesis.pdf"><em>Local Reasoning for Java</em></a>, 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. </p>

<p><a href="http://www.cs.cmu.edu/~neelk/thesis.pdf">My own thesis</a> 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. </p>

CC BY-SA 3.0
2013-01-03T16:13:29.483Z
2013-01-03T16:13:29.483Z
Neel Krishnaswami
<p>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. <a href="http://dl.acm.org/citation.cfm?id=2103663" rel="nofollow" title="ACM link">ACM link</a> or <a href="http://www.doc.ic.ac.uk/~gds/TowardsProgramLogicJavaScriptPOPL2012.pdf" rel="nofollow" title="PDF">direct PDF</a></p>

CC BY-SA 3.0
2013-01-03T11:11:18.760Z
2013-01-03T11:11:18.760Z
brab
<p>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 <a href="http://www.cis.upenn.edu/~bcpierce/sf/Hoare.html" rel="nofollow">http://www.cis.upenn.edu/~bcpierce/sf/Hoare.html</a>). <strong>The question is - is there any line of research where Hoare-style reasoning can be made for programs that creates and deletes objects.</strong> </p>

<p>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.</p>

<p>Are there any references or keywords for furher search into this matter.</p>

<program-verification>
Can Hoare logic be used when objects are created or deleted?
TomR
# Can Hoare logic be used when objects are created or deleted?

(Asked by: username_0 on 2012-12-25)

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.

**Tags:** program-verification

---

## 3 answers

### Answer by username_1 on 2012-12-25. Score: 10

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](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.2984)
2. [Separation Logic](http://en.wikipedia.org/wiki/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](http://www.jstarverifier.org/)


---

### Answer by username_2 on 2013-01-03. Score: 7

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*](http://www.cl.cam.ac.uk/~mjp41/Thesis.pdf), 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](http://www.cs.cmu.edu/~neelk/thesis.pdf) 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.


---

### Answer by username_3 on 2013-01-03. Score: 0

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](http://dl.acm.org/citation.cfm?id=2103663 "ACM link") or [direct PDF](http://www.doc.ic.ac.uk/~gds/TowardsProgramLogicJavaScriptPOPL2012.pdf "PDF")


---

