程式正確性（program correctness）是2018年全國科學技術名詞審定委員會公布的計算機科學技術名詞。
基本介紹
- 中文名：程式正確性
- 外文名：program correctness
- 所屬學科：計算機科學技術
- 公布時間：2018年
定義,出處,
定義
程式是否滿足給定的規約。
出處
《計算機科學技術名詞 》第三版。
程式正確性
相關詞條
- 程式正確性
程式正確性 程式正確性（program correctness）是2018年全國科學技術名詞審定委員會公布的計算機科學技術名詞。定義 程式是否滿足給定的規約。出處 《計算機科學技術名詞 》第三版。
- 程式驗證
程式驗證是指研究程式正確性的理論，即要證明程式達到某種預定目的的任務。美籍匈牙利科學家約翰·馮·諾依曼於1947年發表的論文中就提到程式正確性證明。美國科學家羅伯特·弗洛伊德於1967年系統地提出驗證程式正確性的歸納斷言方法，引起了...
- 程式正確性證明方法
《程式正確性證明方法》是2018年12月上海財經大學出版社出版的圖書，作者是武斌。內容簡介 程式驗證是電腦程式設計領域的前沿研究課題，如何保證程式正確性是計算機科學的一個重大挑戰。本書在前人研究的基礎上，利用符號計算的思想和方法...
- 基於分離邏輯的雲存儲管理程式正確性驗證方法
《基於分離邏輯的雲存儲管理程式正確性驗證方法》是依託北京大學，由王捍貧擔任負責人的面上項目。項目摘要 雲計算作為一種新興的計算模型，代表了計算領域未來的發展方向。而雲存儲作為雲計算的基礎之一，與傳統存儲系統相比有著顯而易見的...
- 多物理程式正確性驗證與可信度確認方法研究
《多物理程式正確性驗證與可信度確認方法研究》是依託北京套用物理與計算數學研究所，由王瑞利擔任項目負責人的面上項目。項目摘要 在國防重大科學與工程高端套用領域，許多現象與事件都是多物理耦合的複雜過程。多物理程式建模與模擬的正確性...
- 結構程式設計(組織正確易讀程式的軟體技術)
程式正確性證明，用數學方法證明程式是否滿足功能規格說明。證明可以是形式的，也可以是非形式的。通常，程式正確性證明總是與逐步精化結合進行。隨著逐步精化，同時加以驗證或程式推導，以得到正確的程式。因此，程式正確性證明是結構程式...
- 程式驗證和規範的形式方法
《程式驗證和規範的形式方法》是1988年科學出版社出版的圖書，作者是H.K.伯格。內容簡介 程式驗證和規範是計算機科學中比較活躍的研究領域。形式化軟體開發方法不僅可有效地指導開發軟體系統的實踐，而且對提高軟體系統的可靠性和可維護性也...
- 拼寫檢查程式
拼寫檢查程式不能識別不常用的人或專用術語，但是它容許你生成自己的個人字典，把自己常用的詞語加進去。簡介 拼寫檢查程式是指將輸入的每個字詞與存儲器里的字典比較，檢查其正確性並在螢幕上顯示差異的電腦程式。拼寫檢查程式可以是一個...
- 程式測試
是指對一個完成了全部或部分功能、模組的計算機程式在正式使用前的檢測，以確保該程式能按預定的方式正確地運行。軟體的正確性尚未得到根本的解決，軟體測試仍是發現軟體錯誤和缺陷的主要手段。為了發現系統中的錯誤，應竭力設計能暴露錯誤...
- 資源感知的程式邏輯理論及資源安全性推理
《資源感知的程式邏輯理論及資源安全性推理》是依託深圳大學，由秦勝潮擔任項目負責人的面上項目。項目摘要 電腦程式的運行離不開系統資源，如記憶體，CPU時間，能源供給等。合理、正確地使用這些系統資源是程式安全性和正確性的一個重要方面...
- 算法正確性
證明算法正確性常用的方法是數學歸納法。若要表明算法是不正確的，只需給出能導致算法不能正確處理的輸入實例即可。算法的正確性證明仍是一項很有挑戰性的工作。在大多數情況下，人們通過程式測試和調試來排錯。程式測試(program testing)...
- 形式程式測試
測試是一種通過執行系統或分析系統來檢查系統正確實現的一種方法。執行測試過程時，將得出的測試結果與規約的結果進行比較來檢查系統的正確性。形式程式測試是指在程式測試中採用形式化方法。形式程式測試可以提高程式測試效率，發現程式錯誤。
- 程式設計語言語義
指稱語義最初被開發為把函式式和順序式程式建模為映射輸入到輸出的數學函式的框架。公理語義學 公理語義學（Axiomatic semantics）是使用數理邏輯來證明程式正確性。程式中的命令的意義描述是通過對程式狀態的斷言（assertion）效果。斷言是...
- 程式調試
程式調試是將編制的程式投入實際運行前，用手工或編譯程式等方法進行測試，修正語法錯誤和邏輯錯誤的過程。這是保證計算機信息系統正確性的必不可少的步驟。編完電腦程式，必須送入計算機中測試。根據測試時所發現的錯誤，進一步診斷，找出...
- 程式設計方法學(學科)
1969 年，Wirth 提出採用“ 自頂向下逐步求精、分而治之” 的原則進行大型程式的設計。其基本思想是：從欲求解的原問題出發，運用科學抽象的方法，把它分解成若干相對獨立的小問題，依次細化，直至各個小問題獲得解決為止。“ 程式正確...
- 程式公正性理論
雖然債權得到實現，案件也結了，但實際已損害了被執行人合法權益，根本沒有達到司法公正。在實踐中，執行程式的這種中立性非常不明顯，從某些方面看甚至是失了這種中立性。1?辦案中的“三同”問題。即當事人與辦案人員同吃、同住、同行...
- 正確性證明
正確性證明 正確性證明（correctness proof）是2018年公布的計算機科學技術名詞。定義 證明程式滿足其規約的過程。出處 《計算機科學技術名詞 》第三版。
- 證明程式
證明程式指的是法律所規定的證明過程中必須遵循的步驟。要在刑事訴訟中查明是否發生了犯罪，誰是犯罪人及其罪責輕重，必須嚴格按照偵察、起訴、審判的程式進行活動。如果缺少其中任何一個環節，證明就不能取得應有的效力。在偵查、起訴、審判...
- 程式合法性研究:以刑事訴訟法為範例
《程式合法性研究：以刑事訴訟法為範例》是2011年法律出版社出版的圖書，作者是李奮飛。內容簡介 本書在充分論證程式合法性正當性的基礎上，結合案例圍繞程式合法性的保障問題一程式違法的遏制和制裁問題進行了系統探討；分析了程式違法的...
- 反彙編程式
反彙編程式 反彙編程式是一種語言轉換程式，它的功能和彙編程式相反，它能把機器語言程式轉換為彙編語言程式。反彙編程式可以用來將二進制機器語言程式返回到彙編語言程式，來查閱目標碼程式的正確性，它也可作為一種“破譯”程式。
- 靜態測試
靜態方法是指不運行被測程式本身，僅通過分析或檢查源程式的語法、結構、過程、接口等來檢查程式的正確性。對需求規格說明書、軟體設計說明書、源程式做結構分析、流程圖分析、符號執行來找錯。靜態方法通過程式靜態特性的分析，找出欠缺和...
- 一種利用圖同構驗證編譯器的方法
（1）ISTec利用反編譯技術由獨立的小組開發從目標程式翻譯到源程式的反編譯器，比較原始碼與目標代碼反編譯後的代碼的一致性，來實現對編譯器的正確性驗證的方式。（2）XavierLeroy帶領的CompCert項目組利用定理證明的形式化方法首次完成了...
- 調試
調試是保證所提供的設備能夠正常運行的必須程式，所有費用由設備提供商負擔。基本信息 詞目：調試 拼音：tiáo shì 含義：1.編好程式後，用各種手段進行查錯和排錯的過程。作為程式的正確性不僅僅表現在正常功能的完成上，更重要的是對...
- 軟體測試——原理、模型、驗證與實踐
第6章程式正確性形式演繹證明 6.1公理化 6.1.1霍爾邏輯及其證明規則 6.1.2霍爾邏輯系統的可靠性和完備性 6.2不變式 6.2.1程式流程圖 6.2.2不變式概念 6.2.3不變式之間的一致性 6.2.4一個更強的屬性 6.2.5流程圖...
- 編程的修煉(2013年電子工業出版社出版的圖書)
作者基於其敏銳的洞察力和長期的實際編程經驗，對基本順序程式的描述和開發中的許多關鍵問題做了獨到的總結和開發。書中討論了順序程式的本質特徵、程式描述和對程式行為（正確性）的推理，並通過一系列從簡單到複雜的程式的思考和開發範例...
