A Comparative Analysis of Heap Specification Approaches

This presentation discusses various approaches to heap specification, including ownership systems, dynamic frames, permissions, and capabilities. It explores challenges related to invariants and frames, showcasing examples from RockBand and Object state specifications. The discussion covers tools like Dafny, Chalice, and Spec#, highlighting their features, strengths, and potential areas for improvement in applying them to heap-manipulating programs.

• Heap Specification
• Ownership Systems
• Dynamic Frames
• Permissions
• Verification

kas_she Follow

Uploaded on Sep 14, 2024 | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

Presentation Transcript

1. Comparing heap models: Ownership, Dynamic frames, Permissions K. Rustan M. Leino RiSE, Microsoft Research Typing, Analysis and Verification of Heap-Manipulating Programs Dagstuhl, Germany 20 July 2009

2. Specification challenges Invariants Describes what holds of an object in its steady state When does an invariant hold? Frames Describes what is being modified or read Goals: Flexibility Conciseness

3. Heap specification approaches Ownership Various type systems JML Spec# Dynamic frames Kassios VeriCool Dafny Permissions, capabilities Boyland et al. Separation logic Chalice

4. Example: RockBand r g Play() :RockBand Invariants: 0 gigs 7 gt.Level .gigs .gt Strum() :Guitar .Level

5. Spec# Object invariant declarations Object state: Mutable Valid Consistent Committed Ownership System of owners, rep objects, and peers Enforced in logic modifies clauses say what fields of mutable and consistent objects are modified :Rock Band mutable :Guitar consistent :GtString :GtString committe d

6. Dafny Sets Functions Ghost state Style of specification Valid() describes steady state footprint set of objects in the aggregate (cf. valid/state paradigm in ESC/Modula-3)

7. Chalice Permissions guide what can be read and written Predicates and functions Valid *) language designed for concurrency

8. Some conclusions Spec# + Intuitive declarations naturally capture common situations; Readonly, frozen - Hard to break out of methodology Dafny + Simple language; Flexible - Verbose; Extension to concurrency? Chalice + Flexible - Simulatenous, different abstraction levels?; Mental overhead

9. Try it for yourself Dafny, Chalice, Boogie available as open source: http://boogie.codeplex.com Spec# available in binary form: http://research.microsoft.com/specsharp and soon also available as open source under academic license: http://specsharp.codeplex.com

10. Bibliography Spec# Vision paper (CASSIS), 2004 Spec# methodology (nee Boogie methodology), 2004 ff. Retrospective paper, 2009 Dafny Model and tutorial (Marktoberdorf), 2008 Chalice Model (ESOP), 2009 Tutorial (FOSAD), 2009 Boogie Boogie 1 architecture paper (FMCO), 2005 Boogie 2 type system and logic, 2009 Boogie 2 language reference manual, 2008 http://research.microsoft.com/~leino/papers.html

11. Boogie C with HAVOC specifications C with VCC specifications Spec# Dafny Chalice Boogie Isabelle/ HOL Simplify Z3 SMT Lib