后續問題:如果“應該/不應”要求被違反,那么該要求位于哪個部分(例如語意、約束)是否重要?.
ISO/IEC 9899:202x (E) 作業草案——2020 年 12 月 11 日 N2596,5.1.1.3 診斷,1:
如果預處理翻譯單元或翻譯單元違反任何語法規則或約束,即使該行為也明確指定為未定義或實作,則一致實作應產生至少一個診斷訊息(以實作定義的方式標識)定義。在其他情況下不需要產生診斷訊息。
結果:違反語意不需要診斷。
問題:“違反語意不需要診斷”的(可能的)理由是什么?
uj5u.com熱心網友回復:
賴斯定理給出了一個可能的基本原理:程式的非平凡語意屬性是不可判定的
例如,除以零是違反語意的;并且您無法僅通過對 C 源代碼的靜態分析來決定它不會發生......
標準不能要求完全檢測這種未定義的行為,即使當然某些工具(例如Frama-C)有時能夠檢測到它們。
另請參閱停機問題。你不應該期望一個 C 編譯器來解決它!
uj5u.com熱心網友回復:
C99 基本原理 v5.10 給出了這樣的解釋:
5.1.1.3 診斷
通過為任何包含語法錯誤或違反約束的程式強制規定某種形式的診斷訊息,該標準執行兩項重要服務。首先,它強調了錯誤程式的概念,因為一致的實作必須將這樣的程式與有效的程式區分開來。其次,它嚴重限制了對一致實作所允許的擴展的性質。
該標準沒有說明診斷訊息的性質,這可能只是“語法錯誤”,沒有提示錯誤發生的位置。(當然,實作必須描述什么翻譯器輸出構成診斷訊息,以便用戶可以識別它。)C89 委員會最終決定,任何超出此級別的診斷活動都是實作質量的問題,并且市場力量將鼓勵更多有用的診斷。盡管如此,C89 委員會認為至少必須診斷出一些重要的錯誤類別,并且指定的類別應該被所有翻譯人員識別。
uj5u.com熱心網友回復:
發生這種情況是因為C 語言的語法是背景關系敏感的,并且對于在喬姆斯基層次結構上使用背景關系無關或更復雜的語法定義的所有語言,必須在語言的語意與其功能之間進行權衡。
C 設計人員選擇為語言提供強大的功能,這就是不可判定性問題在 C 中無處不在的原因。
有像 Coq 這樣的語言試圖消除不可判定的情況,并且它們限制了遞回函式的語意(它們只允許 sigma(原始)遞回)。
轉載請註明出處,本文鏈接:https://www.uj5u.com/qiye/331932.html
