研究生課程_程序語言設(shè)計(jì)原理教程_第17章.ppt

第16章 指稱語義的原理與應(yīng)用,指稱語義學(xué)是christopher strachey和dana scott在1970年提出的。指稱語義學(xué)是christopher strachey和dana scott在1970年提出的。指稱語義學(xué)是christopher strachey和dana scott在1970年提出的。 指稱語義學(xué)的一個顯著特征是: 程序中的每一個短語(表達(dá)式、命令、聲明等)都有其意義。它是與語言的語法結(jié)構(gòu)平行的。每個短語的語義函數(shù)就是短語的指稱意義。其現(xiàn)代名稱為指稱語義學(xué)。 16.1 指稱語義原理 從數(shù)學(xué)的觀點(diǎn)，一個程序可以看作是從輸入到輸出的映射p(i)o，即輸入域(domain)上的值，經(jīng)過程序p變?yōu)檩敵鲇?range)的值。 pd (pp，dd)。 語義域d中的數(shù)學(xué)實(shí)體d, 或以輔助函數(shù)表達(dá)的復(fù)雜數(shù)學(xué)實(shí)體d，稱為該短語的數(shù)學(xué)指稱物，即短語在語義函數(shù)下的指稱語義。 指稱語義描述的是語義函數(shù)映射的后果，不反映如何映射的過程，更沒有過程的時間性。而程序設(shè)計(jì)語言的時間性只能反映到值所表達(dá)的狀態(tài)上。, 語義函數(shù)和輔助函數(shù) 描述二進(jìn)制數(shù)的語義 二進(jìn)制數(shù) numeral := 0 (16.1-a) 1 (16.1-b) numeral 0 (16.1-c) numeral 1 (16.1-d) 我們給出求值的語義函數(shù):將numeral集合中的對象映射為自然數(shù): valuation: numeralnatural (16.2) 按語法的產(chǎn)生式，我們給出以下語義函數(shù): valuation 0= 0 valuation 1 = 1 valuation n0 = 2 valuation n nnumeral valuation n1 = 2 valuation n+ 1,valuation1101 = 2 valuatioin 110+ 1 = 2 (2 valuation 11) + 1 = 2 (2 (2 valuation 1+ 1) + 1 = 2 (2 (2 1 + 1) + 1 = 13 計(jì)算器命令的語義描述 計(jì)算器命令的抽象語法： com := expr= (16.3) expr := num (16.4-a) expr + expr (16.4-b) expr - exp (16.4-c) expr * expr (16.4-d) num := digitnum digit (16.5) digit := 0123456789 (16.6) execute : com lnteger evaluate: expr lnteger sum : integer integer integer difference : integer integer integer product : integer integer integer,以下定義每個短語的語義函數(shù): execute c = execute e= = evaluate e 其中ccom，eexpr。 evaluate n= valuation n (nnum) evaluate e1 + e2 = sum (evaluate e1，evaluate e2) evaluate e1 - e2 = difference (evaluate e1，evaluatee2) evaluate e1 * e2 = product (evaluate e1, evaluate e2) 再定義num的兩個表達(dá)式: valuation d = d (ddigit,dnatural) valuation nd= 10 valuation n+ d execute 40-3*9= =evaluate 40-3*9 =product (evaluate40-3，evaluate9) =product (difference (evaluate 40，evaluate 3)， evaluate9) =product (difference (valuation40，valuation3)， valuation9) =product (difference (40，3)，9) =333,16.1.2 語義域 基本域 character / lnteger / natural / truth-value / unit 用戶可定義枚舉域,以及以基本域構(gòu)造的復(fù)合域。 笛卡兒積域 dd 元素為對偶(x，x)其中xd，xd。 d1d2dn元素為n元組(x1，x2，xn)，其中xidi。 不相交的聯(lián)合域 d+d 元素為對偶(left x，right x)其中xd，xd。 shape=rectangle( realreal ) + circle real + point, 函數(shù)域 dd 例如lntegereven。 f(v) 偏函數(shù)，vv f() 嚴(yán)格的偏函數(shù) f()v 非嚴(yán)格函數(shù) 偏函數(shù)域上元素間具有偏序關(guān)系，偏序關(guān)系的性質(zhì)是: d域若具偏序性質(zhì)，它必須包含唯一的底元素，記為，且d，d為d中任一元素。通俗解釋是d得到的定義比多。是不對應(yīng)任何值的值。 若 x，y d，xy此二元素具有偏序關(guān)系，即y得到的定義比x多。這一般就復(fù)合元素而言，即x中包含的比y多。 若x，y，zd，則偏序關(guān)系必須是: 1 自反的，即有xx; 2 反對稱的，即若xy，yx，必然有x=y; 3 傳遞的，即若xy，yz，必然有xz。, 序列域 序列域d*中的元素是零個或多個選自域d中的元素有限序列，或?yàn)閚il元素，或?yàn)閤s的序列 nil 一般寫法是“ ” anil 一般寫法是“a” busy nil 一般寫法是“busy” 16.1.3 命令式語言的特殊域 存儲域,store = location ( stored storable + undefined + unused) (16.15),empty-store : store (16.16) allocate : store store location (16.17) deallocate : store location store (16.18) update : store location storablestore (16.19) fetch : store locationstorable (16.20) empty_store = loc.unused allocate sto = let loc = any_unused_location (sto) in (sto loc undefined，loc) deallocate (sto，loc) = sto loc unused update (sto，loc，stble) = sto locstored stble fetch (sto，loc) = let stored_value (stored stble) = stble stored_value (undefined) = fail stored_value (unused) = fail in stored-value (sto(loc), 環(huán)境域 environ = ldentifier(bound bindable + unbound) empty-environ : environ bind : ldentifierbindable environ overlay : environenviron environ find : environldentifierbindable enpty-environ = i. unbound bind (i，bdble) = i. if i=i then bound bdble else unbound overlay (env，env) = i. if env (i)/=unbound then env (i) else env (i) find (env，i) = let bound_value (bound bdble) = bdble bound_value (unbound) = in bound_value (env (i),16.2 指稱語義示例 過程式小語言 imp 抽象語法是: command := skip ldentifier := expression let declaration in command command; command if expression then command else command while expression do command expression := numeral false true ldentifier expression + expression expression expression not expression . declaration := const ldentifier = expression var ldentifier : type_denoter type_denoter := bool int, imp的語義域、語義函數(shù)和輔助函數(shù) value = truth_value truth_value + integer lnteger storable = value bindable = value value + variable location execute: command (environstorestore) executec env sto = sto evaluate: expression (environstore value) evaluate e env sto= elaborate: declaration (environstore environstore) elaborate d env sto =,輔助函數(shù)有如前所述的empty-environ，find，overlay，bind，empty-store，allocate，deallocate，update，fetch。以及sum，less，not等輔助函數(shù)。此外，再增加一個取值函數(shù): coerce: storebindablevalue coerce (sto，find (env，i) = val = fetch (sto，loc) imp的指稱語義 execute skip env sto = sto execute i:= e env sto = let val = evaluate e env sto in let variable loc = find (env，i) in update(sto，loc，val) execute let d in c env sto = let (env，sto) = elaborate d env sto in execute c (overlay (env，env) sto,execute c1; c2 env sto = execute c2 env (execute c1 env sto) execute if e then c1 else c2 env sto = if evaluate e env sto = truth_value true then execute c1 env sto else execute c2 env sto execute while e do c= let execute_while env sto = if evaluate e env sto = truth_value true then execute_while env (execute c env sto) else sto in execute_while,elaborate const i = e env sto = let val = evaluate e env sto in (bind (i，value val)，sto) elaborate var i:t env sto = let (sto，loc)= allocate sto in (bind (i，variable loc)，sto),16.3 程序抽象的語義描述 函數(shù)抽象 function = argumentvalue function = argumentstorevalue bind_parameter: formal_parameter(argumentenviron) give_argument : actual_parameter(environargument) 擴(kuò)充imp語法 command := identifier (actual_parametor) expression := identifier (actual_parmenter) declaration := func identifier (formal_parameter) is expression proc ldentifier (formal_paramenter) is command formal_parameter := const identifier: type_denoter actual_parameter := expression,argument = value bindable = value value + variable location + function function 寫imp函數(shù)的指稱語義 bind-parameter i:t arg = bind (i，arg) give-argument e env = evaluate e env 函數(shù)調(diào)用的語義等式如下: evaluate i(ap) env = let function func = find (env，i) in let arg = give_argument ap env in func arg,elaborate fun i(fp) is e env = let func arg = let parenv = bind_parameter fp arg in evaluate e (overlay (parenv，env ) in (bind (i，function func) 過程抽象 procedure = argumentstorestore argument = value bindable = value value + variable location+functionfunction +procedure procedure execute i(ap) env sto=,let procedure proc = find (env，i) in let arg = give_argument ap env sto in proc arg sto elaborate proc i(fp) is c env sto = let proc arg sto = let parent = bind-parameter fp arg in execute c (overlay (parenv env) sto in (bind (i，procedure proc)，sto) 參數(shù)機(jī)制的語義描述 - 常量和變量參數(shù) 先細(xì)化參數(shù)定義語法 formal-parameter := const identifier: type_denoter var identifier : type_denoter actual-p arameter := expression var identifier,bind_parameter : formal_parameter(argumentenviron) give_parameter : actural_parameter(environstoreargument) 形參的語義等式是: bind_parameter const i:t (value val) = bind (i，value val) bind_parameter var i:t (variable loc)= bind(i，variable loc) 實(shí)參的語義等式是: give_argument e env sto = value (evaluate e env sto) give_argument var i env sto = let variable loc = find (env，i) in variable loc,- 復(fù)制參數(shù)機(jī)制 formal_parmeter := value identifier: type_denoter result identifier : type_denoter actual_parameter := expression var identifier copy_in: formal_parameter(argumentstoreenvironstore) copy_in value i:t (value val) sto = let (sto，local) = allocate sto in (bind (i，variable local)，update (sto，local，val) copy-in result i:t (variable loc) sto= let (sto，local)= allocate sto in (bind (i，variable local)，sto) copy_out: formal_parameter(environ argumentstorestore),copy_out value i:t env (vlaue val) sto = sto copy_out result i:t env (variable loc) sto = let variable local = find (env，i) in update (sto，loc，fetch (sto，local) 過程聲明的語義等式作以下修改: elaborateproc (fp) is c env sto= let proc arg sto= let (parenv，sto“) copy_in fp arg sto in let sto = execute c (overlay (parenv，env ) sto“ in copy_out fp parenv arg sto in (bind (i，procedure proc)，sto),- 多參數(shù) function = argument*storevalue procedure = argument* storestore bind_parameter : formal_parameter_list(argument* environ) give_argument:acrual_parameter_list(environ store argament*) - 遞歸抽象 遞歸函數(shù)聲明的語義等式如下: elaborate fun i (fp) is e env= let func arg = let env=overlay (bind (i，function func)，env) in let parenv = bind-parameter fp arg in evaluate e (overlay (parenv，env) in bind (i，function func),16.4 復(fù)合類型 最簡單的復(fù)合變量的語義描述 數(shù)組變量的語義描述 16.5 程序失敗的語義描述 sum: integer integer integer sum (int1，int2) = if abs(int1+int2) =maxint then int1+int2 else sum (，int2)= sum (int1，) = evaluate e1 + e2 env sto = let integer int1 = evaluate e1 env sto in let integer int2 = evaluete e2 env sto in integer (sum (int1，int2),16.6 指稱語義應(yīng)用 指稱語義用于設(shè)計(jì)語言 為一個程序設(shè)計(jì)語言寫指稱語義的步驟是: 分析(所設(shè)計(jì)的)程序設(shè)計(jì)語言的規(guī)格說明寫出抽象語法。 定義該語言的指稱域，并為這些域定義洽當(dāng)?shù)妮o助函數(shù)以模型值上的操作。 建立語義函數(shù)。為抽象語法中的每個短語(即短語類)指定一個域(語義函數(shù)的 輸入域)，定義輸入域到其指稱域的語義函數(shù)。 為每一短語類寫出語義等式。,16.6.2 指稱語義用于程序性質(zhì)研究 上下文約束的靜態(tài)描述 在程序設(shè)計(jì)語言的文法產(chǎn)生的所有句子之中只有一部分是良定義的。語法往往不能給出明確的表示，要依靠上下文約束。 用指稱語義的方法描述程序設(shè)計(jì)語言的上下文約束要建立類型環(huán)境的概念。語言中各類型之總稱即為type域。例如，在前述imp語言中類型域是: type=truth_type + integer_type + var_type + error_type type_environ = identifier(bound type + unbound) equivalent: typetypetruth_value,可測試兩種類型是否等價。 constrain: command(type_environtruth_value) 檢查命令在類型環(huán)境中是否遵從約束，即是否良定義的。 typify: expression(type_environvalue_type) 驗(yàn)明表達(dá)式的類型，即在類型環(huán)境中的具體類型。 declare : declaration(type_environtruth_valuetype_environ) 在類型環(huán)境中給出聲明是良定義的真值, 以及所產(chǎn)生的類型束定。 type_denoted_by: type_denotervalue_type 產(chǎn)生類型指明符的真實(shí)類型。類型環(huán)境域有以下輔助函數(shù): empty_environ : type_environ bind : ldentifier type type_environ overlay: type_environtype_environtype_environ find: type_environidentifiertype 程序推理 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 val = evaluate e env sto in let val variable loc = find (env，i) in update (sto，loc，val) end end execute (letdinc (d，c) env sto = let val (env，sto) = elaborate d env sto in execute c (overlay (env，env) sto end,16.6.3 語義原型 先將抽象語法改寫為ml的datatype 定義: type identifier = string and num eral = string; datatype command = skip ibecomese 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 flase true ide of identifier epluse of expression * expression and declaration= constiise of ldentifier * expression varicolont of ldentifier* typerdenoter and typedenoter= bool int,將域的各等式也轉(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 val = evaluate e env sto in let val variable loc = find (env，i) in update (sto，loc，val) end end execute (letdinc (d，c) env sto = let val (env，sto) = elaborate d env sto in execute c (overlay (env，env) sto end, execute (csemicolonc (c1，c2) env sto = exe