added special syntax to reason about the return value of methods in the post...

added special syntax to reason about the return value of methods in the post condition, added some equivalent mutants (c# code), changed while loops to generate smaller wlp formulas if the loop does not affect the post condition