search

symphonytool / symphony

The Symphony IDE
5 stars 4 forks source link

Backend of POG should use "@" instead of "&" in Symphony #221

Closed pglvdm closed 10 years ago

pglvdm commented 10 years ago

This seems to be an issue when the quick check POG is invoked for all quantified expressions and comprehensions

ldcouto commented 10 years ago

The issue is actually broader than that. CML POs are represented with a VDM AST. They are shown to the user with each node's toString() method which has the VDM characters (such as '&') hardcoded.

The way to fix this is with a CML pretty printer visitor. Doable but time consuming given the size of the tree. For the purpose of discharging POs, of course, this makes no difference.

ldcouto commented 10 years ago

I've implemented a temporary workaround that does string replacements of '&' with '@'. The commit is d5b1854. Not ideal but should be good enough for now.