Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Support for functions #17

Open
3 tasks done
mattulbrich opened this issue Aug 24, 2017 · 2 comments
Open
3 tasks done

Support for functions #17

mattulbrich opened this issue Aug 24, 2017 · 2 comments

Comments

@mattulbrich
Copy link
Owner

mattulbrich commented Aug 24, 2017 •
edited
Loading

In early version, only methods have been considered.
Functions have their own issues:

  • Proof Verification Conditions also for functions
  • Reasoning about well-foundedness
  • Expanding function definitions
@mattulbrich mattulbrich removed the later label Oct 12, 2018
@mattulbrich
Copy link
Owner Author

In principle, all functionality is there.

It remains to provide more test cases and defining a function w/o parameters seems to result in a parsing error currently.

@mattulbrich
Copy link
Owner Author

reads clauses are not supported yet.

  • parse reads clauses
  • add PVCs for reads clauses
  • add reasoning techniques for dynamic frames

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@mattulbrich