Page 144 - 《软件学报》2025年第8期

于涛 等: 基于下推自动机的同步数据流语言可信编译 3567

本文实现的基于下推自动机的编译方法在理论上有良好的可扩展性和语言无关性, 未来可以在编译器扩展性
上进行进一步的研究和实践, 或将该方法扩展应用到其他语言的编译当中.

References:
[1] Benveniste A, Caspi P, Edwards SA, Halbwachs N, Le Guernic P, De Simone R. The synchronous languages 12 years later. Proc. of the
IEEE, 2003, 91(1): 64–83. [doi: 10.1109/JPROC.2002.805826]
[2] Caspi P, Pilaud D, Halbwachs N, Plaice JA. Lustre: A declarative language for real-time programming. In: Proc. of the 14th ACM
SIGACT-SIGPLAN Symp. on Principles of Programming Languages. Munich: ACM, 1987. 178–188. [doi: 10.1145/41625.41641]
[3] Halbwachs N, Caspi P, Raymond P, Pilaud D. The synchronous data flow programming language Lustre. Proc. of the IEEE, 1991, 79(9):
1305–1320. [doi: 10.1109/5.97300]
[4] Berry G, Gonthier G. The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer
Programming, 1992, 19(2): 87–152. [doi: 10.1016/0167-6423(92)90005-V]
[5] Berry G. The foundations of Esterel. In: Proof, Language, and Interaction: Essays in Honour of Robin Milner. Cambridge: The MIT
Press, 2000. 425–454.
[6] Le Guernic P, Gautier T, Le Borgne M, Le Maire C. Programming real-time applications with SIGNAL. Proc. of the IEEE, 1991, 79(9):
1321–1336. [doi: 10.1109/5.97301]
[7] Le Guernic P, Talpin JP, Le Lann JC. Polychrony for system design. Journal of Circuits, Systems and Computers, 2003, 12(3): 261–303.
[doi: 10.1142/S0218126603000763]
[8] Lustre V6 home. http://www-verimag.imag.fr/Lustre-V6.html?lang=en
[9] McCarthy J, Painter J. Correctness of a compiler for arithmetic expressions. In: Mathematical Aspects of Computer Science 19: Proc of
Symposia in Applied Mathematics. American Mathematical Society, 1967. 33−41.
[10] Leroy X. Formal verification of a realistic compiler. Communications of the ACM, 2009, 52(7): 107–115. [doi: 10.1145/1538788.
1538814]
[11] CompCert. http://compcert.inria.fr/
[12] Yang XJ, Chen Y, Eide E, Regehr J. Finding and understanding bugs in C compilers. In: Proc. of the 32nd ACM SIGPLAN Conf. on
Programming Language Design and Implementation. San Jose: ACM, 2011. 283–294. [doi: 10.1145/1993498.1993532]
[13] Paulin C, Pouzet M. Certified compilation of SCADE/Lustre. 2006. https://www.lri.fr/~paulin/lustreincoq.pdf
[14] Bourke T, Brun L, Dagand PÉ, Leroy X, Pouzet M, Rieg L. A formally verified compiler for Lustre. ACM SIGPLAN Notices, 2017,
52(6): 586–601. [doi: 10.1145/3140587.3062358]
[15] Shang S, Gan YK, Shi G, Wang SY, Dong Y. Key translations of the trustworthy compiler L2C and its design and implementation. Ruan
Jian Xue Bao/Journal of Software, 2017, 28(5): 1233–1246 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5213.
htm [doi: 10.13328/j.cnki.jos.005213]
[16] Pnueli A, Siegel M, Singerman E. Translation validation. In: Proc. of the 4th Int’l Conf. on Tools and Algorithms for the Construction
and Analysis of Systems. Lisbon: Springer, 1998. 151–166. [doi: 10.1007/BFb0054170]
[17] Pnueli A, Shtrichman O, Siegel M. Translation validation for synchronous languages. In: Proc. of the 25th Int’l Colloquium. Aalborg:
Springer, 1998. 235–246. [doi: 10.1007/BFb0055057]
[18] van Ngo C, Talpin JP, Gautier T, Le Guernic P, Besnard L. Formal verification of compiler transformations on polychromous equations.
In: Latella D, Treharne H, eds. Proc. of the 2012 Int’l Conf. on Integrated Formal Methods, 2012. 113–127.
[19] van Ngo C, Talpin JP, Gautier T, Le Guernic P. Translation validation for clock transformations in a synchronous compiler. In: Proc. of
the 18th Int’l Conf. on Fundamental Approaches to Software Engineering, 2015. 171–185. [doi: 10.1007/978-3-662-46675-9_12]

附中文参考文献:
[15] 尚书, 甘元科, 石刚, 王生原, 董渊. 可信编译器 L2C 的核心翻译步骤及其设计与实现. 软件学报, 2017, 28(5): 1233–1246. [doi:
10.13328/j.cnki.jos.005213]

附录 A. 形式化验证过程中所使用的符号集

在本文形式化验证过程中所使用的公理系统其符号集如表 A1 所示.