程序設(shè)計(jì)語言理論-在線瀏覽
2024-08-30 07:13本頁面
【正文】 系統(tǒng) – 指稱語義：形式系統(tǒng)的模型 等式、歸約和語義 公理語義 一個等式公理系統(tǒng) ? 約束變元改名公理 （ ?公理 ） – ?x:?.M ? ?y:?.?y?x?M， M中無自由出現(xiàn)的 y 其中 ?N?x?M表示 M中的 x用表達(dá)式 N代換的結(jié)果 – 例如 ?x:?.x ? ?y:?.y ? 函數(shù)應(yīng)用公理 （ ?公理 ） – (?x:?.M)N ? [N/x]M – 例如 (?x:+4) 4 ? [4/x](x+4) ? 4 + 4 等式、歸約和語義 ? 自反公理、對稱性規(guī)則、傳遞性規(guī)則 ? 同余規(guī)則 – 相等的函數(shù)應(yīng)用于相等的變元產(chǎn)生相等的結(jié)果 ? 等式證明規(guī)則允許推導(dǎo)任何一組等式前提的邏輯推論 M1 = M2 N1 = N2 M1 N1 = M2 N2 等式、歸約和語義 操作語義 語言的操作語義可用不同的方式給出 ? 定義一個抽象機(jī) ,通過一系列的機(jī)器狀態(tài)變換來計(jì)算程序 ? 演繹出最終結(jié)果的證明系統(tǒng) – 前面所列的等式公理的單向形式給出了歸約規(guī)則 – 最核心的歸約規(guī)則是 (?)的單向形式 (?x:?.M)N ?? [N/x]M – 通常沒有 ? 歸約規(guī)則： ?x:?.M ?? ?y:?.?y?x?M 等式、歸約和語義 指稱語義 ? 確定語言構(gòu)造 （ 程序 、 語句 、 表達(dá)式等 ） 到指稱物 （ 各種集合 ） 的語義映射 ， 滿足： – 各種語言構(gòu)造的實(shí)例都有對應(yīng)的指稱物 – 復(fù)合構(gòu)造的指稱只依賴于它的子構(gòu)造的指稱 ? 類型化 ?演算的指稱語義 – 每個類型表達(dá)式對應(yīng)到一個集合 – 類型 ? 的項(xiàng)解釋為其值集上的一個元素 – 類型 ? ? ? 的值集是函數(shù)集合，項(xiàng) ?x:?.M解釋為一個數(shù)學(xué)函數(shù) 類型和類型系統(tǒng) ? 類型論 – 為避免集合論悖論而建立起來的數(shù)學(xué)理論 – 主要研究集合的分層、分類方法 – 在程序設(shè)計(jì)語言理論中，類型論是指類型系統(tǒng)的設(shè)計(jì)、分析和研究 ? 類型提供了所有可能值的一種劃分 – 一個類型是一群有某些公共性質(zhì)的值 ? 對于不同的類型系統(tǒng)，類型的多少和值所屬的類型可能不同 類型和類型系統(tǒng) 類型和類型系統(tǒng) ? 類型語言 ：變量都被給定類型 ? 未 類 型化的 語 言 ：不限制變量值的范圍 ? 類型系統(tǒng) – 語言的一個組成部分 – 由一組定型規(guī)則構(gòu)成 ? 類型系統(tǒng)的研究有兩個分支 – 類型系統(tǒng)在程序設(shè)計(jì)語言中的應(yīng)用 – “純類型化 ?演算”和各種邏輯之間的對應(yīng)關(guān)系 類型和類型系統(tǒng) 設(shè)計(jì)類型系統(tǒng)的目的 ? 用來證明程序不會出現(xiàn)不良行為 ? 類型可靠的語言（安全語言） – 所有程序運(yùn)行時都沒有不良行為出現(xiàn) – 類型系統(tǒng)的研究也需要形式化的方法 – 許多語言定義被發(fā)現(xiàn)不是類型可靠的，甚至經(jīng)過類型檢查后接受的程序也會崩潰 ? 顯式類型化的語言： 類型是語法的一部分 ? 隱式類型化的語言 類型和類型系統(tǒng) 類型語言的優(yōu)點(diǎn) ? 開發(fā)時的實(shí)惠 – 可以較早發(fā)現(xiàn)錯誤 – 類型信息具有文檔作用（比程序注解精確，比形式規(guī)范容易理解） ? 編譯時的實(shí)惠 – 程序模塊可以相互獨(dú)立地編譯 ? 運(yùn)行時的實(shí)惠 – 更有效的空間安排和訪問
環(huán)評公示相關(guān)推薦
鄂ICP備17016276號-1