公开(公告)号：CN119597276A

公开(公告)日：2025-03-11

申请号：CN202411499068.9

申请日：2024-10-25

Applicant: 北京计算机技术及应用研究所

Inventor： 华岳桐 ,  张建伟 ,  贾张涛 ,  张霄霄 ,  李浩宇 ,  冯大成 ,  安恒 ,  李福川 ,  孟程昊 ,  陈莉 ,  王磊 ,  王云则 ,  张翠婷

IPC: G06F8/35 ,  G06F8/41

Abstract: 本发明涉及一种结合8114准则的同步数据流语言可信翻译方法，属于代码生成领域。本发明通过对Lustre源代码词法、语法分析和翻译等步骤获取Ctemp中间语言的抽象语法树；遍历Ctemp抽象语法树，针对树结构中的语句中控制流语句、赋值语句设计翻译方法；遍历语句中的表达式，设计添加强制转化的翻译方法，确保语句在语义正确的同时，不存在隐式类型转化；扩展了关于Cltype中类型关系的定理，用于验证类型操作；扩展关于Ctemp语义的强制转化和二元操作的定理，实现语义形式化验证。本发明大幅度提升代码生成工具所生成的C代码对GJB 8114规范的满足性。