Object Models, Heaps and Interpretations
This paper explores the use of object models for specifying verifiable heap invariants. We define a simple language based on sets and relations and illustrate its use through examples. We give formal semantics of the laguage by translation into predicate calculus and interpretation of predicates i...
| Main Authors: | , |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149919 |