Feature/predicates

[alegnani]

• adds array access syntax to every variable (not only heap) in annotations: acc(some_array[0]
• definitions of predicates in top-level annotations: /* @ predicate P(a: Int) { a == 0 } @*/
• fold/unfold statements as annotations /*@ fold P(x) @*/
• predicates in method pre/postconditions: /*@ requires P(x) @*/
• heap arg automatically added to predicates: /*@ fold P(x) @*/ -> fold P(heap, x)
• unfolding in expression implemented: /*@ requires unfolding IO() in heap[42] == 17 @*/
• closes #12