编程语言编译器开发工具【免费下载链接】grammars-v4Grammars written for ANTLR v4; expectation that the grammars are free of actions.项目地址https://gitcode.com/gh_mirrors/gr/grammars-v4点击查看免费下载导读本文以 grammars-v4 仓库中的 z/ 目录 为主线系统讲解一个基于 ANTLR4、遵循 ISO/IEC 13568:2002 标准含勘误实现的 Z Notation 文法。ZZermelo-Fraenkel 形式化规格语言是一种用于软件规格说明的规范描述语言其难点在于运算符是上下文敏感的——同一个名称记号token在不同上下文中扮演不同角色。本仓库通过词法分析 → 运算符模板解析与记号重写 → 正式解析的三阶段流程解决这一问题。读完本文你将掌握 Z 文法在 ANTLR4 中的整体架构、上下文相关运算符如何通过监听器改写成专用记号、关联性associativity如何借助语义谓词与assoc选项实现以及仓库内测试示例的使用方式与已知限制。一、项目概览与文件布局仓库的 z/ 目录下包含完整的三段式文法与配套 Java 支持代码ZLexer.g4ISO 13568 的完整词法定义覆盖盒式字符、括号、关键词、数学工具包符号等ZOperatorParser.g4专用解析器仅用于识别运算符模板段落并驱动监听器把NAME记号改写为对应的运算符记号ZParser.g4正式解析器在改写后的记号流上构建完整的 Z 语法树ZOperatorListener.java改写逻辑的核心负责类型映射与关联性记录ZSupport.java运行时支持类为解析器提供关联性查询Test.java.alternative演示运算符模板拼接 三阶段解析 语法树 GUI 展示的完整流程examples/ 与 failed_examples/测试样例与暂未通过的样例。按照 desc.xml 的声明该文法目标语言为 JavaANTLR 版本要求为^4.7pom.xml 中通过antlr4-maven-plugin同时编译ZLexer.g4、ZParser.g4、ZOperatorParser.g4三个文法并开启visitor与listener生成测试入口点为specification规则样例目录为examples/。二、标准依据与设计动机2.1 以 ISO/IEC 13568:2002 为准README.md 明确说明本文法基于 ISO 标准ISO/IEC 13568:2002含 技术勘误实现。ISO 标准采用Unicode 数学字符集本仓库词法严格遵循该字符编码约定例如盒式字符─U2500ZED、┌U250CSCH、╷U2577AX在 ZLexer.g4 中触发mode(Z)切换括号字符采用 U27EA/27EB《》与 U2989/298A⦉⦊等数学双角括号与绑定括号见 ZLexer.g4换行符NLCHAR使用 U2028 LINE SEPARATOR见 ZLexer.g4这与标准中用 LINE SEPARATOR 替代 LINE FEED的勘误一致数学工具包字符集合工具包、关系工具包、函数工具包、数字工具包、序列工具包在 ZLexer.g4 中被分类成片段规则fragment。词法实现还处理了 Unicode 一般类别WS跳过所有 General Category Zs 的空白DIGIT区分十进制数字Nd与非十进制数字Nl/NoLETTER覆盖拉丁字母、希腊字母、双字母记号如 、ℕ以及任意 L* 类 UCS 字符见 ZLexer.g4。2.2 运算符的上下文敏感性Z 语言的一个关键特性是section段中声明的运算符模板operator template会在后续文本中被当作运算符使用但词法阶段无法区分——例如模板(_ ∪ _)中的∪和正文表达式S ∪ T中的∪词法上都是同一个符号。ISO 标准规定运算符的绑定fixity前缀/中缀/后缀/无缀和关联性由模板声明决定这使 Z 的语法是上下文相关的。本仓库的设计策略不是把这种上下文相关性强塞进单个文法那样会产生大量歧义而是将解析拆成两个阶段这正是 README.md 的核心内容。三、三阶段解析架构从原始文本到语法树根据 README.md 与 Test.java.alternative完整流程如下原始 .utf8 输入 │ ① ZLexer 词法分析 ▼ 通用记号流NAME 记号尚未区分 │ ② ZOperatorParser 解析 ZOperatorListener 改写 ▼ 改写后的记号流运算符 NAME 被替换为 PRE/POST/I/L/EL/ER/… 等专用记号 │ ③ ZParser 正式解析 ▼ Z 语法树可 GUI 展示3.1 第一步词法分析ZLexer词法器把输入切分为基础记号。值得注意的是 ZLexer.g4 末尾定义了一组占位记号PREP/PRE/POSTP/POST/IP/I/LP/L/ELP/EL/ERP/ER/SREP/SRE/SRP/SR/ES/SS它们全部映射到NAME规则。这意味着初始词法阶段把所有标识符一律当成普通名称至于它将来是前缀运算符、中缀运算符还是参数化运算符留待第二阶段按上下文决定。词法器内部还实现了换行敏感处理shouldNL()方法根据当前记号与下一记号判断换行是否有效见 ZLexer.g4避免在括号后、关键词后等位置产生无意义的换行记号。3.2 第二步运算符模板解析与记号改写ZOperatorParser ZOperatorListenerZOperatorParser.g4 只关心specification → section/paragraph结构中的运算符模板段落section支持继承式section name parents formals与基础式section name见 ZOperatorParser.g4paragraph识别operatorTemplate、公理描述AX、模式定义SCH等其中只有OperatorTemplateParagraph需要深度处理见 ZOperatorParser.g4operatorTemplate分为关系运算符模板relation、函数运算符模板function与泛型运算符模板generic并支持prec优先级数值与assocleftassoc/rightassoc修饰见 ZOperatorParser.g4模板的固定性通过prefixTemplate/postfixTemplate/infixTemplate/nofixTemplate表达其中_ARGUMENT表示参数占位符NAME表示运算符名见 ZOperatorParser.g4。改写的核心在 ZOperatorListener.java类型映射表监听器维护了relationMap、functionMap、prefixMap、postfixMap、infixMap、nofixMap六张映射表见 ZOperatorListener.java把基础占位记号映射为语义上正确的记号类型。例如relationMap把PRE→PREP、I→IP、EL→ELP而functionMap保持PRE→PRE、I→I不变——这说明关系运算符与函数运算符在正式解析阶段使用不同的记号类别ZParser中的relation规则只匹配带P后缀的记号见 ZParser.g4。替换动作replaceType()调用((WritableToken)token).setType(...)就地修改记号类型同时把token.getText() → 新类型记录进associations映射若当前模板是右结合则把运算符文本追加进rightAssociativity集合见 ZOperatorListener.java。固定性判断replaceFixName()通过反射调用上下文上的NAME()、argName()、listName()方法确定运算符是简单名字、参数化有_参数占位还是列表化_,列表占位并据此决定把名字改写为L/ER/SR等相应记号见 ZOperatorListener.java。关联性记录exitAssoc()在遇到rightassoc时置位isRightAssoc随后被替换的运算符文本都会被加入rightAssociativity见 ZOperatorListener.java。3.3 第三步正式解析ZParser改写后的记号流交给 ZParser.g4 解析。此时ZParser可以从记号本身区分运算符角色其表达式规则覆盖 Z 语言的核心构造谓词合取/析取/蕴涵/等价/否定/全称与存在量词含唯一存在以及关系运算符应用见 ZParser.g4表达式模式合取/析取、模式蕴涵、模式组合⨟、模式管道⨠、模式隐藏\、模式投影⨡、前置条件pre、笛卡尔积、幂集、λ 函数构造、μ 确定描述、let 替换、绑定选择、元组、集合延拓与集合抽象、绑定扩展、泛型实例化等见 ZParser.g4段落给定类型、公理描述、模式定义、泛型公理/模式、水平定义、泛型水平定义、自由类型、猜想含泛型猜想、运算符模板见 ZParser.g4运算符应用通过prefixName/postfixName/infixName/nofixName与对应的prefixApp/postfixApp/infixApp/nofixApp规则处理各种固定性应用见 ZParser.g4。四、关联性与语义谓词README 中的核心探讨4.1 右结合assocrightREADME.md 给出两个示例模板| expression {ZSupport.isLeftAssociative(_input)}? I expression #InfixLeftApplicationExpression | assocright expression I expression #InfixRightApplicationExpression第一行表示当运算符不是右结合时走左结合分支并在进入该分支前用语义谓词ZSupport.isLeftAssociative(_input)做守卫第二行用 ANTLR4 内建assocright选项声明右结合分支。isLeftAssociative的实现非常简洁见 ZSupport.javapublic static SetString rightAssociativity new HashSetString(); static boolean isLeftAssociative(TokenStream tokens) { return !rightAssociativity.contains(tokens.get(tokens.index()).getText()); }即当前待预测的运算符文本若已被ZOperatorListener记录为右结合则谓词返回 false左结合分支被排除解析器选择assocright分支。rightAssociativity集合在 Test.java.alternative 中通过ZSupport.rightAssociativity ol.rightAssociativity;从监听器注入。同样的技巧还用于relation规则中的((ELEMENT_OF | EQUALS_SIGN | IP) expression)分支见 ZParser.g4。4.2 左结合谓词位置为何有效README 作者引用了 StackOverflow 的讨论原帖并坦率提出一个疑问语义谓词不在规则最左端理论上 ANTLR4 预测阶段可能忽略它。但实际测试表明关联性处理看起来是正确工作的。README 的推测是解析器可能先按默认方式解析左操作数表达式之后因谓词生效而回退/旁落到下一条规则。从仓库源码看这种能工作但原理存疑的状态与 ANTLR4 的 SLL/LL 预测机制、谓词求值时机有关。这里如实转述 README 的表述不夸大其结论本实现依赖语义谓词位置的特殊性来实现结合性切换作者本人也并未完全确定其内部机理。4.3 优先级precedence未实现README 明确指出一个已知限制运算符模板中指定的优先级值prec未被考虑。作者不确定 ANTLR4 能否实现这一点。从 ZParser.g4 看operatorTemplate规则确实接受并解析prec NUMERAL优先级数值但在表达式文法中没有对应的优先级驱动——即优先级信息只是被语法上接受没有被用于指导表达式归约。五、运行方式与测试样例5.1 编译与测试在仓库根目录执行 Maven 即可对 z/ 编译测试依据 pom.xmlmvn -pl z testantlr4-maven-plugin会生成三个文法对应的 Java 解析器antlr4test-maven-plugin以specification为入口对 z/examples/ 下的样例做解析验证。5.2 演示程序 Test.javaTest.java.alternative 是完整的端到端演示注意它是.alternative后缀运行时需按需重命名为Test.java并放到合适包结构下用SequenceInputStream把standard_toolkit_operator_templates.utf8ISO 标准 Annex B 的运算符模板清单拼接到目标规格文本之前——这是让正文运算符能被正确识别的前提ZLexer词法分析 →ZOperatorParser解析出运算符模板树ParseTreeWalker驱动ZOperatorListener改写记号流用associations映射统一把WritableToken类型更新注入rightAssociativity后重置记号流交给ZParser生成正式语法树用 ANTLR 的TreeViewer在 Swing GUI 中展示解析树。5.3 样例说明examples/18 个通过的样例其中standard_toolkit_operator_templates.utf8的对应内容位于 failed_examples/standard_toolkit_operator_templates.utf8其余样例如birthdaybook.utf8Spivey 经典 BirthdayBook 规格见 examples/birthdaybook.utf8源自 CZTCommunity Z Tools测试用例failed_examples/暂未通过解析的样例包括Sched.utf8、ch5.utf8、posix.utf8、tokeneer_41_2_all_merged_for_parsing.utf8等 9 个文件——它们可作为研究文法力所不及之处的素材。从 standard_toolkit_operator_templates.utf8 可以看到真实的运算符模板语法section prelude ─generic (ℙ _)└ ─function 30 leftassoc (_ _)└以及section relation toolkit parents set toolkit B.5.3 Maplet ─function 10 leftassoc (_ ↦ _)└ B.5.7 Relational composition ─function 40 leftassoc (_ ⨾ _)└这直观展示了generic/function/relation三类模板、prec数值、leftassoc/rightassoc关键字与_占位符的书写格式。六、已知限制与注意事项综合 README.md 与源码本实现存在以下明确限制父段parents感知的模板映射未实现Test.java.alternative 总是把整个standard_toolkit_operator_templates.utf8拼接到输入前。而 ISO 规范要求只有无父段的 section 才映射整个工具包若某 subsection 被列作父段则应只映射其局部模板。这一行为尚未实现。优先级不生效prec数值虽被解析但不参与表达式归约见 4.3。关联性机制的原理存在不确定性README 作者明确表示不确定它是如何工作的见 4.2。部分真实世界规格无法解析failed_examples/中的样例如 tokeneer 工程合并文件说明文法尚不能覆盖全部 Z 用法使用时应先验证目标输入是否在支持范围内。七、总结grammars-v4 的 z/ 目录提供了一个可运行的、严格对照 ISO/IEC 13568:2002 的 Z 文法参考实现。其核心设计决策是词法→运算符模板改写→正式解析的三阶段流水线词法器按 Unicode 标准切词并保留NAME泛化记号ZOperatorListener依据运算符模板把记号重写成语义类别ZParser在改写流上无歧义地构造语法树。关联性通过语义谓词 assocright选项的组合实现优先级与父段感知映射则留作已知限制。对于研究 ANTLR4 上下文相关文法设计、Z 形式化方法工具链如与 CZT 对标或需要解析 Z 规格的工程实践本仓库都是一个值得对照的起点。赞分享编程语言编译器开发工具【免费下载链接】grammars-v4Grammars written for ANTLR v4; expectation that the grammars are free of actions.项目地址https://gitcode.com/gh_mirrors/gr/grammars-v4点击查看免费下载相关推荐DIFData Interchange Format语法解析基于 ANTLR4 的 dif 文法实现与实战指南DIFData Interchange Format语法解析基于 ANTLR4 的 dif 文法实现与实战指南 本文以 grammars v4 仓库中的编程语言编译器开发工具grammars-v4 项目 PDNPortable Draughts NotationANTLR4 文法解析实战指南grammars v4 项目 PDNPortable Draughts NotationANTLR4 文法解析实战指南 导读 本文基于 grammars v编程语言编译器开发工具GKE TPU v6e 节点 vbar_control_agent OOM 故障特征识别指南serial console、tpu-device-plugin 与高频轮询三大信号GKE TPU v6e 节点 vbar_control_agent OOM 故障特征识别指南serial console、tpu device plugin编程语言编译器开发工具上一篇拯救者Y7000系列BIOS隐藏选项一键解锁告别黑苹果安装障碍释放硬件全部潜能下一篇TVBoxOSC视频弹幕功能与其他观众互动交流创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考