Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
why3
why3
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 125
    • Issues 125
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 15
    • Merge Requests 15
  • Operations
    • Operations
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
  • Why3
  • why3why3
  • Issues
  • #261

Closed
Open
Opened Jan 28, 2019 by GARCHERY Quentin@qgarcherDeveloper

Giving names to requires and ensures

Allow to give names to the pre/post-conditions, for example using the syntax :

requires arg_pos { x > 0 }

This would be helpful because :

  • it would make it clear where this axiom comes from when proving VCs
  • it would make the proof more robust as the axiom name would not change from H12 to H13 when adding another requires
Edited Jan 28, 2019 by GARCHERY Quentin
To upload designs, you'll need to enable LFS and have admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: why3/why3#261