基于翻译确认的面向侧面静态语义检查和验证方法及系统

本申请涉及一种基于翻译确认的面向侧面静态语义检查和验证方法和系统，其中，方法包括：确定两种前端中间语言L和M，并分别设置侧面A的静态语义良好性谓词；获取M对应的影子语言M'，并确定M'到M的匹配映射，并构建一个从L到M'的翻译并进行静态语义性质检查的检查函数；将检查函数和匹配映射依序联合在一起，生成一个满足侧面A的静态语义性质检查需求的翻译确认程序，并将翻译确认程序附加于从L至M的翻译过程之后，以进行面向侧面A的静态语义检查和正确性验证。由此，解决了现有的可信编译器中静态语义分析/检查过程的正确性验证缺乏考虑通用情形，以及因处理新增静态语义特性可能引发的前端翻译及其证明过程大面积修改等问题。