代數(shù)語(yǔ)義學(xué)-資料下載頁(yè)
2025-10-08 19:52本頁(yè)面
【導(dǎo)讀】令、聲明等)都有其意義。它是與語(yǔ)言的語(yǔ)法結(jié)構(gòu)平行的。其現(xiàn)代名稱為指稱語(yǔ)義學(xué)。即輸入域上的值，經(jīng)過(guò)程序P變?yōu)檩敵鲇虻闹?。稱為該短語(yǔ)的數(shù)學(xué)指稱物，即短語(yǔ)在語(yǔ)義函數(shù)下的指稱語(yǔ)義。，更沒(méi)有過(guò)程的時(shí)間性。而程序設(shè)計(jì)語(yǔ)言的時(shí)間性只能反映到值。所表達(dá)的狀態(tài)上。其中C∈Com，E∈Expr。=product(difference(evaluate〖40〗，evaluate〖3〗)，用戶可定義枚舉域,以及以基本域構(gòu)造的復(fù)合域。Dn元素為n元組(x1，x2，…，xn)，其中xi∈Di。D+D'元素為對(duì)偶其中x∈D，x'∈D'。D→D'例如lnteger→Even。偏函數(shù)域上元素間具有偏序關(guān)系，偏序關(guān)系?·D域若具偏序性質(zhì)，它必須包含唯一的底元素，記為⊥，且⊥≤d，通俗解釋是d得到的定義比⊥多。[1]自反的，即有x≤x;[2]反對(duì)稱的，即若x≤y，y≤x，必然有x=y;[3]傳遞的，即若x≤y，y≤z，必然有x≤z。a’·nil∥一般寫法是“a”
【正文】 n→(Type_Environ→Truth_Value Type_Environ) 在類型環(huán)境中給出聲明是良定義的真值 , 以及所產(chǎn)生的類型束定。 type_denoted_by: Type_Denoter→Value_Type 產(chǎn)生類型指明符的真實(shí)類型。類型環(huán)境域有以下輔助函數(shù) : empty_environ : Type_Environ bind : ldentifier Type →Type_Environ overlay: Type_Environ Type_Environ→Type_Environ find: Type_Environ Identifier→Type 程序推理 C。 ship ≡ C 。 要證明相等，即指出兩端指稱一樣即可 : execute 〖 C。 skip〗 env sto = execate 〖 skip〗 env (execute C env sto) = execute C env sto 將域的各等式也轉(zhuǎn)成 ML的 datatype定義 : type Location = int。 datatype Value= truthvalue of bool ｜ integer of int。 type Stroeable = Value。 datatype Bindable = value of Value ｜ variable of Location。 再寫出具體函數(shù)定義 : fun execute (skip) env sto = sto ｜ execute (IbceomesE(I， E)) env sto = let val val39。 = evaluate E env sto in let val variable loc = find (env， I) in update (sto， loc， val39。) end end ｜ execute (letDinC (D， C)) env sto = let val (env39。， sto39。) = elaborate D env sto in execute C (overlay (env39。， env)) sto39。 end 語(yǔ)義原型 先將抽象語(yǔ)法改寫為 ML的 datatype 定義 : type Identifier = string and Num eral = string。 datatype Command = skip ｜ IbeesE of Identifier * Expression ｜ letDinC of Declaraton * Command ｜ CsemicolonC of Command * Command ｜ ifEthenCelseC of Expressiion * Command * Command ｜ whileEdoC of Expression * Command and Expression = num of Numeral ｜ flase39。 ｜ true39。 ｜ ide of Identifier ｜ EplusE of Expression * Expression and Declaration= constIisE of Ldentifier * Expression ｜ varIcolonT of Ldentifier* Typerdenoter and Typedenoter= bool39。 ｜ int39。 將域的各等式也轉(zhuǎn)成 ML的 datatype定義 : type Location = int。 datatype Value= truthvalue of bool ｜ integer of int。 type Stroeable = Value。 datatype Bindable = value of Value ｜ variable of Location。 再寫出具體函數(shù)定義 : fun execute (skip) env sto = sto ｜ execute (IbceomesE(I， E)) env sto = let val val39。 = evaluate E env sto in let val variable loc = find (env， I) in update (sto， loc， val39。) end end ｜ execute (letDinC (D， C)) env sto = let val (env39。， sto39。) = elaborate D env sto in execute C (overlay (env39。， env)) sto39。 end ｜ execute (CsemicolonC (C1， C2)) env sto = execute C2 env (execate C1 env sto) ｜ execute (if E then C else C (E， C1， C2)) env sto = if valuate E env sto = truthvalue true then execute C1 env sto else execute C2 env sto ｜ execute (whileEdoC (E， C))= let fun executewhile env sto = if evaluate E env sto = truthvalue true then executewhile env (execute C env sto ) else sto in executewhile end and evaluate (num N) env sto = integer (valuation N) ｜ evaluate (false39。) env sto = truthvalue false ｜ evaluate (true39。) env sto = truthvalue true ｜ evaluate (ide I) env sto = coerce (sto， find (env， I )) ｜ evaluate (EplusE( E1， E2 )) env sto = let val integer int1 = evaluate E1 env sto in let val integer int2 = evaluate E2 env sto in integer (sum ( int1， int2 ) ) end end ｜ ... and elaborate (constIisE ( I， E )) env sto= let val val39。=evaluate E env sto in (bind (I， value val’ )， sto) end ｜ elaborate (varIcolonT( I， T )) env sto= let val (sto39。， loc)=allocate sto in ( bind ( I， variable loc )， sto39。) end and valuation (N) = integer (stringtoint N) 以上按 IMP 抽象語(yǔ)法套寫語(yǔ)義函數(shù) execute, evaluate， elaborate. 還要把輔助函數(shù)改寫為 ML: fun coerce ( sto， value val39。)= val39。 ｜ coerce ( sto， vatiable loc ) = fetch ( sto， loc ) 設(shè)置初始條件運(yùn)行 ML程序 有了以上定義，即可運(yùn)行抽象語(yǔ)法樹的 ML解釋器，例如 : val env0=...。 //初始環(huán)境 val sto0=...。 //初始存儲(chǔ) val prog=...。 //一條 IMP命令的抽象語(yǔ)法樹 execute prog env0 sto0。
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號(hào)-1