Added Return Value Patterns

Added a function to fit identifiers on the return values of functions. For example,

int[n]{r} foo(int[n] x)
  | _all_V_(_gt_VxS_(r, 0))
{
    return x;
}

is now valid, with the return value in the postcondition being mapped to r.