There is an issue I have in the source code of Rodin 2.7. I found the
"getSyntaxTree()" method in "BecomesSuchThat" class under package
"org.eventb.core.ast" only dispatch "boundNames" to the getSyntaxTree's
chain, rather than "boundNamesBelow"(which concats the local primed
variables along with "boundNames"). This causes some inaccuracy of the
"getSyntaxTree" method, i.e., some of boundIdentifier cannot be resolved
underneath the BecomesSuchThat node.
I wonder is this the correct behaviour or a bug. Could anybody confirm
that? Thank you very much.
Get latest updates about Open Source Projects, Conferences and News.