Please enable JavaScript.

Coggle requires JavaScript to display documents.

Chapter3 Semantics(語義) (Static Semantics (Attribute Grammars (屬性文法)…

- - - - 用途
        
        和meaning無關
        
        關注程式的語法是否合法(而非語義)
        
        e.g. 在A =A+B中，檢查 “=” 左邊的變數與右邊的加法運算結果type是否相符
      - 緣由
        
        有些結構很難用BNF描述
        
        e.g Java中浮點數的值無法被只怕給整數型別的變數
    - - 從Parse Tree思考
        
        儲存相關資訊
        
        Attributes
        
        A(x)屬性集合由兩個不相交的集合組成
        
        :fire::fire::fire:p.3-41圖
        
        S(X)
        
        synthesized attributes
        
        合成屬性 (向上傳遞資訊)
        
        I(X)
        
        inherited attributes
        
        繼承屬性 (向下、跨分支傳遞資訊)
        
        每個symbol都應該儲存type
        
        規範資訊流通
        
        Semantic functions
        
        attribute computation functions
        
        檢查資訊
        
        Predicate functions
        
        用來檢查正確性
        
        對某rule中所有的nonterminal，所有相關的predicate function均必須為true，此rule才可被用在derivation
    - - 說明
        
        是樹葉節點的合成屬性
        
        只有葉節點才有，且其值來自外界
    - - 定義
        
        parse tree中的所有屬性都已被計算完成
    - - 優點
        
        屬性文法可用來正式定義一個語言，並可當做編譯器產生系統的輸入
      - 缺點
        
        很難描述一個程式語言所有的語法及固定語意(耗記憶體、不容易寫、剖析代價大)
    - - excepted_type (inherited)
      - actual_type (synthesized)
      - :fire: p.46~49 example
- - - - 說明
        
        用高階語言描述低階語言，使人容易了解
        
        分為2 level
        
        自然操作語意
        
        關注最後結果
        
        結構操作語意
        
        關注單一語句的精準度
        
        想在高階語言用操作語意，就需要一個虛擬機器
        
        使用直譯器
        
        用硬體做 : 太貴
        
        用軟體做 : machine-dependent、太複雜、無法傳輸
        
        替代方案 : 電腦模擬
        
        建一個翻譯器 : 把source code 轉成機器碼
        
        建模擬器
      - 基本過程(:fire::fire::fire: 3-70圖片)
        
        1st step : 設計合適的中繼語言 (需清晰，像機器碼就太難懂了)
        
        需要替中繼語言建一個虛擬機(or直譯器)。
        
        ↑自然操作語意，需要。結構操作語意，可不用。
      - 評估
        
        優點
        
        適用非正式使用 (e.g. 使用手冊、教科書、教程式語言)
        
        為使用者有效、簡單地描述語義
        
        缺點
        
        用於正式使用，則會變得非常複雜 (e.g. VDL)
      - VDL
        
        用來定義PL/I的語義。卓越的技術成就，但幾乎沒有實際用途。
    - - 特點
        
        Based on 遞迴函式理論
        
        最抽象的語義描述方法
      - 方法(:fire::fire::fire: 3-73圖片)
        
        利用mapping function把語言實例對應到數學物件(e.g.整數)
      - 說明
        
        State :　目前所有的變數與其值
        
        Example : :fire::fire::fire: 3-82圖片
      - 評估
        
        可用來證明程式的＊＊正確性＊＊
        
        提供嚴謹的方法來思考程式
        
        可用於編譯器生成系統
    - - 特點
        
        特點
        
        利用數學推論來証明程式的正確性
        
        Based on 數學邏輯（謂詞計算）
        
        Assertions
        
        precondition : 在statement之前
        
        postcondition : 在statement之後
        
        weakest precondition : 若postcondition成立，則w.p.成立 (保證成立的precondiction)。根據post推出的pre
        
        程式證明過程
        
        把程式的期望結果當作last statement的postcondition
        
        ->計算last statement的w.p
        
        ->再把w.p當作前一statement的postcondition，循環至程式開頭
        
        ->若開頭的precondition成立
        
        ->程式正確
        
        推理規則
        
        若antecedent(前因)符合，則可推斷出consequence(後果)成立
        
        General form : :fire::fire::fire: p.90圖
        
        Axiom(公理)
        
        定義
        
        被假設為真的 logical statement
        
        無須前因的推理規則
        
        The Rule of Consequence : :fire::fire::fire: p.94
        
        The Inference Rule for Sequences : :fire::fire::fire: p.95
        
        Pretest Loops
        
        example
        
        {P} while B do S end {Q}
        
        The inference rule for computing the precondition
        
        {(I and B)}S{I}/ {I} while B do S {I and (not B)}
        
        Loop Invariant
        
        條件
        
        P->I (I為loop invariant)
        
        {I and B} S {I}
        
        (I and (not B)) -> Q
        
        The loop terminates
        
        評估
        
        發展某些語言的推理規則很困難。解決方法為設計具有公理規則的語言，且該種語言應該很小、簡單
        
        適用於驗證正確性