Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 169
    • Issues 169
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 24
    • Merge requests 24
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #94
Closed
Open
Issue created Aug 18, 2017 by Ralf Jung@jungOwner

iInv without Hclose

I've been talking about accessors today with @janno and @pythonsq. One place where having "actual" accessors might be useful is to avoid "Hclose"-style assumptions. I think we can prototype how that would look like by playing with iInv.

Particularly, I suggest that we get rid of the last parameter of iInv (the name of the "Hclose"), and instead have it add that as an obligation to the postcondition. So, if the goal starts out being WP e {{ v, Q }}, then when opening inv N I it becomes WP e {{ v, \later I * Q }}. Similar things happen when the goal is a view shift.

@robbertkrebbers @jjourdan what do you think? How hard would it be to implement this? We'd probably want a new typeclass generalizing things that can be in the goal when doing iInv. I fear that typeclass will be much like the infamous "frame shift assertions"...

Edited Aug 18, 2017 by Ralf Jung
Assignee
Assign to
Time tracking