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
  • #211
Closed
Open
Issue created Oct 01, 2018 by Joseph Tassarotti@jtassaroDeveloper

Masks are coPsets in the Coq development, not arbitrary subsets of natural numbers

The appendix suggests that masks for updates and weakest preconditions may be arbitrary sets (it does not say so explicitly when defining fancy updates, but on p. 29 the camera used for "enabled" invariants is said to be P(N)). However, in the Coq code, the representation used for masks is coPset. @robbertkrebbers says that coPsets are used so that the representation has extensional equality, but that in principle the constructions all could work with arbitrary sets.

It seems like either the discussion in the appendix should be changed to coPset as well (in order to stick to the claim that everything is verified), or an explanatory note should be given. Unfortunately, it is not so easy to concisely describe coPsets: they contain all finite and cofinite sets, and are closed under various set operations. However, as @jung points out, the namespace "suffix" construction is not so clearly derivable just from the closure properties.

Assignee
Assign to
Time tracking