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

Add support for expression operators: !in and fresh #91

Open
mattulbrich opened this issue Oct 12, 2018 · 0 comments
Open

Add support for expression operators: !in and fresh #91

mattulbrich opened this issue Oct 12, 2018 · 0 comments
Assignees
@mattulbrich
Labels
enhancement

Comments

@mattulbrich
Copy link
Owner

!in, fresh(o) can be parsed, but is not supported during term creation.

For fresh: Implement it as a function $fresh(heap, object) that allows one to specify the heap. This should be prettyprinted as fresh(o)@heap if not the standard heap.

This fresh function should acrually replace the function isCreated and be its negation.
The Dafny language supports fresh, hence that should go into our logic.
@mattulbrich mattulbrich self-assigned this Oct 12, 2018
mattulbrich added a commit that referenced this issue Oct 15, 2018
@mattulbrich
towards #91: Introducing !in
f53e66b 
Adding to parser, translation and test cases.
Adding test cases for yet unresolved fresh(.) expressions
mattulbrich added a commit that referenced this issue Oct 17, 2018
@mattulbrich
replace "$isCreated" by "fresh" (#91)
e723430 
which is its negation, but included in the Dafny language.
mattulbrich added a commit that referenced this issue Oct 19, 2018
@mattulbrich
adding translation for fresh (#91)
8e91cc4 
some test cases fail
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@mattulbrich mattulbrich

Labels
enhancement
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@mattulbrich