公理語義（axiomatic semantics）是2018年公布的計算機科學技術名詞，出自《計算機科學技術名詞 》第三版。
基本介紹
- 中文名：公理語義
- 外文名：axiomatic semantics
- 所屬學科：計算機科學技術
- 公布時間：2018年
定義,出處,
定義
用邏輯斷言及其推理系統來描述程式設計語言的語義, 其典型代表是由托尼·霍爾（Tony Hoare）提出的霍爾公理語義。
出處
《計算機科學技術名詞 》第三版。
公理語義
相關詞條
- 公理語義
公理語義（axiomatic semantics）是2018年公布的計算機科學技術名詞，出自《計算機科學技術名詞 》第三版。定義用邏輯斷言及其推理系統來描述程式設計語言的語義, 其典型代表是由托尼·霍爾（Tony Hoa...
- 公理語義學
在公理語義學中，使用公式{x=κ}P{x=κ!}表示程式P的這一部分含義:若P執行前x的值等於κ,則P執行完畢後 x的值等於κ!。程式P執行前的條件(x=κ)稱為P的前置條件，執行後的條件(x=κ!)稱為P的後置條件。這類公式稱為歸納...
- 程式設計語言語義
公理語義學（Axiomatic semantics）是使用數理邏輯來證明程式正確性。程式中的命令的意義描述是通過對程式狀態的斷言（assertion）效果。斷言是邏輯語句——帶變數的謂詞，而這些變數定義了程式的狀態。公理語義的套用也非常廣泛，早在 1973 ...
- 形式語義學
典型的公理語義方法是Hoare公理系統。代表人物有R.W.Floyd和C.A.R Hoare;如果掌握了形式語義學裡面的數學理論、方法和概念，就可以用它們去創造規則、刻畫規則和證明規則，從而可以描述和推導各類程式設計語言的各種成分和性質。發展形式...
- 查詢語言語義學
指稱語義:主要刻畫數據加工的結果， 而不是加工過程的細節；公理語義: 用公理化的方法描述程式對數據的加工；代數語義: 把程式設計語言看作是刻畫數據和加工數據的一種抽象數據類型 ， 使用研究抽象數據類型的代數方法 ，來描述程式設計...
- 形式語義學基礎與形式說明
《形式語義學基礎與形式說明》是2010年科學出版社出版的圖書，作者是屈延文。本書介紹了指稱語義學、代數語義學、操作語義學與公理語義學的基本內容及其套用，並介紹了並發程式設計語言各流派的語義模型和新一代計算機計算模型的理論問題。內...
- 相對正確公理
相對正確公理，可以用來推導網路空間不依賴先驗知識的感知機理。其通俗表述為：“人人都存在這樣或那樣的缺點，但極少出現獨立完成同樣任務時，多數人在同一個地點、同一時間、犯完全一樣錯誤的情形”。有研究者將其命名為“相對正確”公理...
- 正則性公理
在一些沒有正則公理的 ZFC 變體中，非良基集合是可以存在的。在這種系統中工作的時候，不必然良基的集合叫做超集合。明顯的，如果A∈A，則A是非良基超集合。超集合的理論已經套用於計算機科學（進程代數和最終語義）、語言學（情景理論）...
- 程式設計語言理論
1.2等式、歸約和語義 1.2.1公理語義 1.2.2操作語義 1.2.3指稱語義 1.3類型和類型系統 1.3.1類型和類型系統 1.3.2類型語言的優點 1.4歸納法 1.4.1表達式上的歸納 1.4.2證明上的歸納 1.4.3良基歸納 習題 第2章可...
- 程式理論
指稱語義，把程式作為論域間的泛函以便刻畫程式的執行數學結果。公理語義，用公理化方法刻畫程式與被加工數據的邏輯關係。代數語義，把程式執行的結果定義為滿足某種公理體系的代數結構。程式理論對形式語義的需求，促進了論域、偏序以及範疇...
- Anna語言導論
6.1公理語義 6.2轉換語義與實現 6.3基本工具 7結束語 附錄 Ada語法 第二部分：Anna語言參考手冊 0作者前言 1Anna基本概念 1.1虛擬Ada行文 1.2標註 1.3標註的語義 1.3.1程式狀態 1.3.2斷言與Anna核 1.3.3Anna程式的一致...
- 程式語言理論
1969年，Tony Hoare介紹了Hoare邏輯，這是一種公理語義。1969年，威廉·艾爾文·霍華德（William Alvin Howard）觀察到，一種稱為“自然演繹”的“高級”證明系統可以直接在其直覺主義版本中被解釋為計算模型的類型變體，稱為lambda演算。
- 程式設計語言概念(第9版)
動態語義 102 3.5.1操作語義 103 3.5.2指稱語義 104 3.5.3公理語義 108 小結 118 文獻注釋 119 複習題 119 習題 120 第4章詞法分析和語法分析 124 4.1概述 124 4.2詞法分析 125 4.3語法分析問題 132 4.3.1語法分析...
- 計算機科學的數學基礎
第十七章 程式的指稱語義 17.1 把程式看作函式 17.2 序列程式結構的程式函式 17.3 分支程式結構的程式函式 17.4 循環程式結構的程式函式 17.5 循環程式的正確性證明 第十八章 程式的公理語義 18.1 程式的公理語義 18.2 霍爾...
- 理論計算機科學
而形式語義的研究自60年代以來雖有不少研究工作者從事這方面的工作，提出幾種不同的語義理論，主要是操作語義學、指稱語義學或稱數學語義學、公理語義學和代數語義學，但仍沒有一種公認在軟體技術中夠用的形式語義學，因而需要提出一種更...
- 變遷系統
操作語義學 操作語義學是計算機科學中的一個概念，它是使得電腦程式在數學上更加嚴謹的一種手段。其它類似的手段包括提供形式語義學，包括公理語義學和指稱語義。一個計算機語言的操作語義描述一段合理的程式是怎樣被理解為一系列計算機步驟...
- 左正康(江西師範大學教授)
主持完成國家自然科學基金項目“基於代數結構及公理語義的泛型約束方法研究”(61462039)；主持完成的江西省自然科學基金項目“Apla中泛型約束方法與套用研究”(20142BAB217023)結題評價為“優”；主持完成國家自然科學基金重大國際（地區）...
- 多類型時序邏輯程式設計
研究多類型MSVL的類型系統、模型語義、操作語義、公理語義、類型安全性和語義之間等價性。開發多類型MSVL的解釋器，實現對多類型時序邏輯程式的類型檢查、建模、仿真和驗證。結題摘要 時序邏輯程式設計是目前一種廣泛使用的程式設計模式，對...
- 程式靜態分析
程式分析中的形式化方法一般指利用純粹嚴格的數學方法對軟體、硬體進行分析的理論及技術。這些數學方法包括符號語義、公理語義、操作語義和抽象解釋。1952年提出的Rice定理指出，任何關於程式分析的問題都是不可判定的。因此，不存在任何一種...
- 程式設計語言與編譯:語言的設計和實現
第6章 形式語義學簡介 6.1 引言 6.2 形式語義學分類 6.3 公理語義學簡介 6.4 指稱語義學簡介 習題6 下篇 程式設計語言的實現(編譯)第7章 編譯概述 7.1 引言 7.2 翻譯和編譯 7.3 解釋 7.4 編譯步驟 習題7 第8章 詞法...
- 複合性原理
指稱語義 在計算機科學中，指稱語義（英語：Denotational semantics）是通過構造表達其語義的(叫做指稱(denotation)或意義的)數學對象來形式化計算機系統的語義的一種方法。程式語言的形式語義的其他方法包括公理語義和操作語義。指稱語義方式最...
- 進程代數
另外，公理語義學還研究和尋求適用於描述程式語義、便於語義推導的邏輯語言。例如，用時態邏輯定義的語言的公理語義又稱為時態語義。典型的公理語義方法是Hoare公理系統。定義 進程代數英文為：process algebra，在英文中，這個詞組中的process...
- 軟體構架師
1、加強數理邏輯知識，掌握公理語義，能夠通過邏輯演算找出構架的問題。2、注重專業化，不要指望一個構架師什麼類型的軟體都能搞，既然主要靠經驗，就要專業化。3、學習開發案例，找到以前的設計文檔來分析問題。從需求-〉構架-〉詳細設計...
- 段振華(西安電子科技大學計算理論與技術研究所所長)
研究該語言的操作語義和公理語義。開發該語言的一個解釋器。研究該語言在並發、實時和混合系統中的套用。研究架構時序邏輯在網際網路計算及嵌入式系統中的套用。該研究對提高軟體系統的形式驗證的自動化程度、提高軟體的可靠性和安全性具有積極...
