Allow inclusion of pre-state "\old" in specifications

[bjkeller]

The "parsing" of operation specifications currently does not support the use of pre-state in post-conditions. The plan is to allow pre-state expressions with immutable value to be included in a post-condition using the notation \old(expression). The expression(s) would be evaluated before the operation is called, and the values saved in the PostCondition object to be used in evaluation of the post-condition.