Link pure method expressions to the corresponding method exit PPT

[GoogleCodeExporter]

Linking pure method expressions to their corresponding method exit PPT may 
reduce the inference of redundant contracts.

In the example below, the postcondition \result > 0 would be inferred for 
Foo.PositiveNumber(), and the precondition f.PositiveNumber() > 0 would be 
inferred for the precondition of DoSomething.

class Foo {
   int PositiveNumber() { ... }
}


class Bar {
   void DoSomething(Foo f){ ... }
}

Original issue reported on code.google.com by [email protected] on 11 Jun 2013 at 10:40

[GoogleCodeExporter]

Original comment by [email protected] on 14 Jun 2013 at 2:55

• Added labels: Priority-Low
• Removed labels: Priority-Medium