codespecs / daikon-dot-net-front-end

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

Link expressions to their respective Type's object invariant #111

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago
Celeriac infers a lot of expressions at method points that are actually object 
invariants. Each expression needs to have a link to its type's Object Invariant 
so that they contribute to the calculation of the object invariant.

By including an object invariant PPT for every type, even those not in the 
assembly, object invariant can be inferred in the general case.

Original issue reported on code.google.com by Todd.Sch...@gmail.com on 20 Aug 2013 at 7:05

GoogleCodeExporter commented 9 years ago

Original comment by Todd.Sch...@gmail.com on 20 Aug 2013 at 7:05

GoogleCodeExporter commented 9 years ago
Implemented in 3a267e40c805

Original comment by Todd.Sch...@gmail.com on 1 Sep 2013 at 5:48