search

symphonytool / symphony

The Symphony IDE
5 stars 4 forks source link

POG quantifying too many times over function parameters #259

Closed ldcouto closed 10 years ago

ldcouto commented 10 years ago

Given a function:

f:int->int
f(x)== 5/x
pre x <>0

You will get a PO that quantifies twice over x: forall x @ forall x .... Presumably the POG is looking at the pre_f arguments and quantifying them, uselessly.

ldcouto commented 10 years ago

Fixed in overturetool/overture@660a972

joey-coleman commented 10 years ago

It looks like there are six PO tests in symphony that fail due to the removal of duplicated quatifications (and probably just need their results regenerated):

e.c.p.tests.BasicTest:

e.c.p.tests.ModelsTest:

ldcouto commented 10 years ago

Good catch. I'll take care of it tomorrow. Been stuck traveling all day. On 9 Jul 2014 14:12, "Joey Coleman" notifications@github.com wrote:

It looks like there are six PO tests in symphony that fail due to the removal of duplicated quatifications (and probably just need their results regenerated):

e.c.p.tests.BasicTest:

  • FuncPostCondition.cml
  • FunctionApply.cml
  • Subtype_Inv.cml

e.c.p.tests.ModelsTest:

  • AllThePOs.cml
  • Dwarf.cml
  • GM-06.cml

— Reply to this email directly or view it on GitHub https://github.com/symphonytool/symphony/issues/259#issuecomment-48461750 .

ldcouto commented 10 years ago

Turns out I had fixed this (7941c13 and 3cb4c69) but did not push it. Closing again.