[1] |
Wang Ji, Zhan Nai-jun, Feng Xin-yu,et al.Overview of formal methods[J].Journal of Software,2019,30(1):33-61.(in Chinese)
|
[2] |
Gu Tian-long. Formal methods of software development[M].Beijing:Higher Education Press,2005.(in Chinese)
|
[3] |
Chinese Academy Sciences.Chinese disciplinary development strategy·Software science and engineering [M].Beijing:Science Press,2021.(in Chinese)
|
[4] |
Gu Su-mei, Yang Qing-hong. Research and application of strategy for developing circular invariants for 2-class series problems[J].Journal of Jiangxi Normal University (Natural Science Edition),2020,44(3):307-312.(in Chinese)
|
[5] |
Rushby J M,Von Henke F.Formal verification of algorithms for critical systems[J].IEEE Transactions on Software Engineering,1993,19(1):13-23.
|
[6] |
Shi H P,Shi H H,Xu S H.Algorithm design through the optimization of reuse-based generation[C]∥Proc of the 38th National Conference of Theoretical Computer Science,2020:14-32.
|
[7] |
Michael J B,Dinolt G W,Drusinsky D.Open questions in formal methods[J].IEEE Annals of the History of Computing,2020,53(5):81-84.
|
[8] |
You Z,Xue J Y,Zuo Z K.Unified formal derivation and automatic verification of three binary-tree traversal non-recursive algorithms[J].Cluster Computing,2016,19(4):2145-2156.
|
[9] |
Xue J Y,You Z,Hu Q M,et al.PAR:A practicable formal method and its supporting platform[C]∥Proc of International Conference on Formal Engineering Methods,2018:70-86.
|
[10] |
Runge T R,Schaefer I,Cleophas L,et al.Tool support for correctness-by-construction[C]∥Proc of International Conference on Fundamental Approaches to Software Engineering,2019:25-42.
|
[11] |
Dijkstra E W.A discipline of programming [M].Englewood Cliffs:Prentice Hall,1976.
|
[12] |
Chaudhari D L,Damani O.Introducing formal methods via program derivation[C]∥Proc of ACM Conference on Innovation & Technology in Computer Science Education,2015:266-271.
|
[13] |
Chaudhari D L, Damani O. Combining top-down and bottom-up techniques in program derivation[C]∥Proc of International Symposium on Logic-Based Program Synthesis and Transformation,2015:244-258.
|
[14] |
Kourie D G,Watson B W.Correctness-by-construction approach to programming[M].Berlin:Springer Science & Business Media,2012.
|
[15] |
Si X J,Dai H J,Raghothaman M,et al.Learning loop invariants for program verification[C]∥Proc of the 32nd International Conference on Neural Information Processing Systems,2018:7762-7773.
|
[16] |
Shi Hai-he,Xue Jin-yun.Development of a set of reliable search algorithm programs based on PAR[J].Journal of Computer Research and Development,2010(S1):212-216.(in Chinese)
|
[17] |
Shi Hai-he,Xue Jin-yun.PAR-based formal development of algorithm[J].Chinese Journal of Computers,2009,32(5):138-147.(in Chinese)
|
[18] |
Xie Wu-ping,Xue Jin-yun.Research on generation system from Radl algorithm to Apla program[J].Journal of Computer Research and Development,2014,51(4):856-864.(in Chinese)
|
[19] |
Zuo Zheng-kang, Xue Jin-yun.Research on generic constraints of Apla[J].Journal of Software,2015,26(6):1340-1355.(in Chinese)
|
[20] |
Zuo Zheng-kang, Liu Zhi-hao, Huang Qing. A comparative study of generic features of Apla and programming languages[J].Journal of Jiangxi Normal University (Natural Science Edition),2019,43(5):454-461.(in Chinese)
|
[21] |
Wang Chang-jing,Xue Jin-yun.Research on relative correctness of Radl formal specification[J].Journal of Software,2013,24(4):715-729.(in Chinese)
|
|
附中文参考文献:
|
[1] |
王戟,詹乃军,冯新宇,等.形式化方法概貌[J].软件学报,2019,30(1):33-61.
|
[2] |
古天龙.软件开发的形式化方法[M].北京:高等教育出版社,2005.
|
[3] |
中国科学院.中国学科发展战略·软件科学与工程[M].北京:科学出版社,2021.
|
[4] |
吉素梅,杨庆红.2类数列问题循环不变式开发策略研究与应用[J].江西师范大学学报(自然科学版),2020,44(3):307-312.
|
[16] |
石海鹤,薛锦云.一组基于PAR的高可靠查找算法程序开发[J].计算机研究与发展,2010(S1):212-216.
|
[17] |
石海鹤,薛锦云.基于PAR的算法形式化开发[J].计算机学报,2009,32(5):138-147.
|
[18] |
谢武平,薛锦云.Radl算法到Apla程序的生成系统[J].计算机研究与发展,2014,51(4):856-864.
|
[19] |
左正康,薛锦云.Apla中泛型约束机制研究[J].软件学报,2015,26(6):1340-1355.
|
[20] |
左正康,刘志豪,黄箐,等.Apla程序设计语言泛型特性比较研究[J].江西师范大学学报(自然科学版),2019,43(5):454-461.
|
[21] |
王昌晶,薛锦云.Radl形式规格说明相对正确性研究[J].软件学报,2013,24(4):715-729.
|