Chalice syntax for sets, backpointers etc.

Feb 25, 2013 at 11:53 AM
I forked the Chalice project to add Chalice syntax for:
  • permissions within quantifiers
  • sets
  • aggregates (only "sum" is currently supported)
  • backpointers
For these changes I introduced four new keywords: set, sum, emptyset, and tracked. The first two cause problems with some test cases that use them as identifiers. I modified these test cases.

Currently, Chalice will produce an AST tree when given a program with these syntactical extensions. However, it will not try to verify a program with any of these features; it will report that they are currently not supported.

In my projects, I (and/or student(s)) will extend chalice2sil to understand this syntax and translate it appropriately and then Silicon to handle the new features. I suggest that, for uniformity, any extension to the VCG Chalice follows the same syntax. If you agree, but you don't like (something about) the syntax, please let me know.

(Attention: chalice.bat was modified by mistake and I don't know how to revert this change in Codeplex).