search

codespecs / daikon-dot-net-front-end

Celeriac .NET Front-End for Daikon
Other
9 stars 1 forks source link

Link pure method expressions to the corresponding method exit PPT #105

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
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 Todd.Sch...@gmail.com on 11 Jun 2013 at 10:40

GoogleCodeExporter commented 9 years ago

Original comment by Todd.Sch...@gmail.com on 14 Jun 2013 at 2:55