Nội dung được dịch bởi AI, chỉ mang tính chất tham khảo
Đấu tranh với những điều bất khả thi bằng Coq: Xác thực chính thức một thuật toán biên dịch cho các phép di chuyển song song
Tóm tắt
Bài viết này mô tả việc xác thực chính thức một thuật toán biên dịch, chuyển đổi các phép di chuyển song song (các phép gán song song giữa các biến) thành một chuỗi các phép di chuyển cơ bản có ngữ nghĩa tương đương. Hai đặc tả khác nhau của thuật toán được đưa ra: một đặc tả quy nạp và một đặc tả hàm, mỗi đặc tả đều đi kèm với chứng minh tính đúng đắn. Một chương trình hàm sau đó có thể được truy xuất và tích hợp trong trình biên dịch Compcert đã được xác thực.
Từ khóa
#xác thực chính thức #thuật toán biên dịch #di chuyển song song #Coq #CompcertTài liệu tham khảo
Appel, A.W.: Compiling with Continuations. Cambridge University Press (1992)
Balaa, A., Bertot, Y.: Fonctions récursives générales par itération en théorie des types. In: Journées Francophones des Langages Applicatifs 2002, pp. 27–42. INRIA (2002)
Barthe, G., Forest, J., Pichardie, D., Rusu, V.: Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. In: Proceedings of the 8th International Symposium on Functional and Logic Programming (FLOPS’06). Lecture Notes in Computer Science, vol. 3945, pp. 114–129. Springer (2006)
Bertot, Y., Castéran, P.: Interactive theorem proving and program development—Coq’Art: the calculus of inductive constructions. EATCS Texts in Theoretical Computer Science. Springer (2004)
Bertot, Y., Grégoire, B., Leroy, X.: A structured approach to proving compiler optimizations based on dataflow analysis. In: Types for Proofs and Programs, Workshop TYPES 2004. Lecture Notes in Computer Science, vol. 3839, pp. 66–81. Springer (2006)
Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: FM 2006: International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 4085, pp. 460–475. Springer (2006)
Coq Development Team: the Coq proof assistant. Software and documentation available at http://coq.inria.fr/ (1989–2007)
Filliâtre, J.C.: Verification of non-functional programs using interpretations in type theory. J. Funct. Program. 13(4), 709–745 (2003)
Filliâtre, J.C.: The Why software verification tool. Software and documentation available at http://why.lri.fr/ (2003–2007)
Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd Symposium Principles of Programming Languages, pp. 42–54. ACM Press (2006)
Leroy, X., Doligez, D., Garrigue, J., Vouillon, J.: The Objective Caml system. Software and documentation available at http://caml.inria.fr/ (1996–2007)
Letouzey, P.: A new extraction for Coq. In: Types for Proofs and Programs, Workshop TYPES 2002. Lecture Notes in Computer Science, vol. 2646, pp. 200–219. Springer (2003)
May, C.: The parallel assignment problem redefined. IEEE Trans. Softw. Eng. 15(6), 821–824 (1989)
Sethi, R.: A note on implementing parallel assignment instructions. Inf. Process. Lett. 2(4), 91–95 (1973)
Welch, P.H.: Parallel assignment revisited. Software Practice and Experience 13(12), 1175–1180 (1983)