[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Interpreting of "ん" as "±" (or something else?)



I’ve recently tested how well PVS handles Japanese. I was pleased to see that in general it handles it well. However, one surprise I encountered was in the following bit of PVS code:

exampleJapanese: THEORY
BEGIN

真(p_しません: bool): bool =
  p_しません;

しません(p_偽: bool): bool =
  NOT (p_偽);

END exampleJapanese

When I try to parse the theory, I get “Found '±' when expecting ')” when it encounters the first “ん”. If I change that line and the line below it to use “n” instead of “ん”, I then get the error “Found '!id!' when expecting 'END” for the second function. If I then also replace that “ん” with “n”, then the theory parses fine. My current work around is to simple perform that replacement (since “n” is actually pretty close to “ん”).

Is this a known issue, and is there any fix in the works? This is not a high-priority issue for me, but I thought I’d bring it to your attention in case it’s not already known.

Best Regards,
Ben Hocking