代數(shù)語義學(xué)ppt課件

1、代數(shù)語義學(xué)代數(shù)語義學(xué)實(shí)際根底實(shí)際根底函數(shù)式描畫方法函數(shù)式描畫方法程序設(shè)計(jì)言語程序設(shè)計(jì)言語方式語義方式語義指稱語義學(xué)指稱語義學(xué)操作語義學(xué)操作語義學(xué)公理語義學(xué)公理語義學(xué)代數(shù)代數(shù)功能功能執(zhí)行執(zhí)行邏輯邏輯 關(guān)系關(guān)系模型模型離散數(shù)學(xué)離散數(shù)學(xué)程序設(shè)計(jì)言語程序設(shè)計(jì)言語方式語義方式語義編譯原理編譯原理程序設(shè)計(jì)言語程序設(shè)計(jì)言語實(shí)際實(shí)際根底根底語義方式化語義方式化語法方式化語法方式化軟件開發(fā)方法軟件開發(fā)方法程序設(shè)計(jì)言語程序設(shè)計(jì)言語方式語義方式語義程序設(shè)計(jì)方法程序設(shè)計(jì)方法程序設(shè)計(jì)言語了解程序設(shè)計(jì)言語了解籠統(tǒng)才干籠統(tǒng)才干Formal MethodFormal SpecificationFormal Verificat

2、ion第九章第九章 指稱語義的原理與運(yùn)用指稱語義的原理與運(yùn)用指稱語義學(xué)是Christopher Strachey和Dana Scott在1970年提出的。指稱語義學(xué)的一個(gè)顯著特征是: 程序中的每一個(gè)短語(表達(dá)式、命令、聲明等)都有其意義。它是與言語的語法構(gòu)造平行的。每個(gè)短語的語義函數(shù)就是短語的指稱意義。其現(xiàn)代稱號(hào)為指稱語義學(xué)。 16.1 指稱語義原理從數(shù)學(xué)的觀念，一個(gè)程序可以看作是從輸入到輸出的映射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é)指稱物，即短語在

3、語義函數(shù)下的指稱語義。指稱語義描畫的是語義函數(shù)映射的后果，不反映如何映射的過程，更沒有過程的時(shí)間性。而程序設(shè)計(jì)言語的時(shí)間性只能反映到值所表達(dá)的形狀上。 語義函數(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集合中的對(duì)象映射為自然數(shù): valuation: NumeralNatural (16.2)按語法的產(chǎn)生式，我們給出以下語義函數(shù): valuation 0= 0 valuation 1 = 1 valuation N0 =

4、 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ì)算器命令的籠統(tǒng)語法： Com := Expr= (16.3) Expr := Num (16.4-a) Expr + Expr (16.4-b) Expr - Exp (16.4-c) Expr * Expr (16.4-d) Nu

5、m := 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 以下定義每個(gè)短語的語義函數(shù): execute C = execute E= = evaluate E 其中CCom，EExpr。 evaluate N= valuation N (NNum) evalu

6、ate E1 + E2 = sum (evaluate E1，evaluate E2) evaluate E1 - E2 = difference (evaluate E1，evaluateE2) evaluate E1 * E2 = product (evaluate E1, evaluate E2)再定義Num的兩個(gè)表達(dá)式: valuation D = D (DDigit,DNatural) valuation ND= 10 valuation N+ D execute 40-3*9= =evaluate 40-3*9 =product (evaluate40-3，evaluate9) =

7、product (difference (evaluate 40，evaluate 3)， evaluate9) =product (difference (valuation40，valuation3)， valuation9) =product (difference (40，3)，9) =33316.1.2 16.1.2 語義域語義域 根本域根本域 Character / lnteger / Natural / Truth-Value / Character / lnteger / Natural / Truth-Value / UnitUnit 用戶可定義枚舉域用戶可定義枚舉域, ,以

8、及以根本域構(gòu)造的復(fù)合域。以及以根本域構(gòu)造的復(fù)合域。 笛卡兒積域笛卡兒積域 D DD D 元素為對(duì)偶元素為對(duì)偶(x(x，x)x)其中其中xDxD，xDxD。 D1 D1D2D2DnDn元素為元素為n n元組元組(x1(x1，x2x2，xn)xn)，其中，其中xiDixiDi。 不相交的結(jié)合域不相交的結(jié)合域 D+D D+D 元素為對(duì)偶元素為對(duì)偶(left x(left x，right x)right x)其中其中xDxD，xDxD。 shape=rectangle( Real shape=rectangle( RealReal ) + circle Real + Real ) + circle R

9、eal + pointpoint 函數(shù)域 DD 例如lntegerEven。 f(v) 偏函數(shù)，vV f() 嚴(yán)厲的偏函數(shù) f()v 非嚴(yán)厲函數(shù) 偏函數(shù)域上元素間具有偏序關(guān)系，偏序關(guān)系的性質(zhì)是: D域假設(shè)具偏序性質(zhì)，它必需包含獨(dú)一的底元素，記為，且d，d為D中任一元素。通俗解釋是d得到的定義比多。是不對(duì)應(yīng)任何值的值。 假設(shè) x，y D，xy此二元素具有偏序關(guān)系，即y得到的定義比x多。這普通就復(fù)合元素而言，即x中包含的比y多。 假設(shè)x，y，zD，那么偏序關(guān)系必需是: 1 自反的，即有xx; 2 反對(duì)稱的，即假設(shè)xy，yx，必然有x=y; 3 傳送的，即假設(shè)xy，yz，必然有xz。 序列域 序列域

10、D*中的元素是零個(gè)或多個(gè)選自域D中的元素有限序列，或?yàn)閚il元素，或?yàn)閤s的序列 nil 普通寫法是“ anil 普通寫法是“a Busy nil 普通寫法是“Busy16.1.3 命令式言語的特殊域 存儲(chǔ)域 3 7 ? ?stoloc1 loc2 . . . . . loc8Store = Location ( stored Storable + undefined + unused) (16.15)empty-store : Store (16.16) allocate : Store Store Location (16.17) deallocate : Store Location S

11、tore (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) =

12、 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 : EnvironldentifierBindabl

13、eenpty-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 16.2 指稱語義例如指稱語義例如 過程式小言語過程式小言語 IMP IMP籠統(tǒng)

14、語法是籠統(tǒng)語法是: : Command := Skip Command := Skip ldentifier := Expression ldentifier := Expression let Declaration in Command let Declaration in Command Command; Command Command; Command if Expression then Command else Command if Expression then Command else Command while Expression do Command while Expr

15、ession do Command Expression := Numeral Expression := Numeral false false true true Ldentifier Ldentifier Expression + Expression Expression + Expression Expression Expression Expression Expression not Expression not Expression . . Declaration := const ldentifier = Expression Declaration := const ld

16、entifier = Expression var ldentifier : Type_denoter var ldentifier : Type_denoter Type_denoter := bool Type_denoter := bool int int IMP的語義域、語義函數(shù)和輔助函數(shù) Value = truth_value Truth_Value + integer lnteger Storable = Value Bindable = value Value + variable Location execute: Command (EnvironStoreStore) exe

17、cuteC 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ù)。此外，再添加一個(gè)取值函數(shù): coerce: StoreBindableVal

18、ue 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) stoe

19、xecute 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 stoexecute while E do C= let execute_while env sto = if evaluate E env sto = truth_value true then execute_while env

20、(execute C env sto) else sto in execute_whileelaborate 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 16.3 程序籠統(tǒng)的語義描畫程序籠統(tǒng)的語義描畫 函數(shù)籠統(tǒng)函數(shù)籠統(tǒng) Function = ArgumentValue Function = Argumen

21、tValue Function = ArgumentStoreValue Function = ArgumentStoreValue bind_parameter: Formal_Parameter(ArgumentEnviron) bind_parameter: Formal_Parameter(ArgumentEnviron) give_argument : Actual_Parameter(EnvironArgument) give_argument : Actual_Parameter(EnvironArgument) 擴(kuò)展擴(kuò)展IMPIMP語法語法 Command := Command

22、 := Identifier (Actual_Parametor) Identifier (Actual_Parametor) Expression := Expression := Identifier (Actual_Parmenter) Identifier (Actual_Parmenter) Declaration := Declaration := func Identifier (Formal_Parameter) is func Identifier (Formal_Parameter) is Expression Expression proc ldentifier (For

23、mal_paramenter) is Command proc ldentifier (Formal_paramenter) is Command Formal_Parameter := const Identifier: Type_Denoter Formal_Parameter := const Identifier: Type_Denoter Actual_parameter := Expression Actual_parameter := Expression Argument = Value Bindable = value Value + variable Location +

24、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 i

25、n evaluate E (overlay (parenv，env ) in (bind (I，function func) 過程籠統(tǒng) 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

26、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 :

27、= Expression var Identifierbind_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 = valu

28、e (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

29、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)

30、 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

31、 arg sto in (bind (I，procedure proc)，sto)- 多參數(shù)Function = Argument*StoreValue Procedure = Argument* StoreStorebind_parameter : Formal_Parameter_List(Argument* Environ) give_argument:Acrual_Parameter_List(Environ Store Argament*) - 遞歸籠統(tǒng)遞歸函數(shù)聲明的語義等式如下: elaborate fun I (FP) is E env= let func arg = let e

32、nv=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 16.4 復(fù)合類型復(fù)合類型最簡(jiǎn)單的復(fù)合變量的語義描畫最簡(jiǎn)單的復(fù)合變量的語義描畫暫不思索函數(shù)和過程籠統(tǒng)，只添加最簡(jiǎn)單的復(fù)合量對(duì)偶暫不思索函數(shù)和過程籠統(tǒng)，只添加最簡(jiǎn)單的復(fù)合量對(duì)偶(A:T1,B:T2).(A:T1,B:T2).先擴(kuò)展籠統(tǒng)語法：先擴(kuò)展籠統(tǒng)語法：Command := Command := V_name

33、:= Expression V_name := Expression Expression := Expression := V_name V_name (Expression,Expression) (Expression,Expression) V-name := Identifier V-name := Identifier fst V_name fst V_name 相當(dāng)于相當(dāng)于V(1) V(1) snd V_name snd V_name 相當(dāng)于相當(dāng)于V(2) V(2) Type_denoter := bool Type_denoter := bool int int |(Type_

34、denoter|(Type_denoter，Type_denoter) Type_denoter) 對(duì)偶值本身是一個(gè)域?qū)ε贾当旧硎且粋€(gè)域: :Pair_Value = ValuePair_Value = ValueValue Value 對(duì)偶變量的域：對(duì)偶變量的域：Pair_Variable = VariablePair_Variable = VariableVariableVariable Value = truth_value Truth_Value + integer Integer + pair_value Pair_ValueStorable = truth_value Truth_

35、Value + integer IntegerVariable = simple_variable Location + pair_variable Pair_Variable輔助函數(shù)：fetch_variable: StoreVariable Value update_variable: StoreVariableValue Store fetch_variable(sto，simple_variable loc) = fetch(sto，loc) fetch_variable(sto，pair_variable (var1，var2) = pair_value(fetch_variable

36、(sto，var1),fetch-variable (sto，var2) update_variable(sto,simple_variable loc，stble ) = update (sto,loc,stble) update_variable (sto,pair_variable (var1,var2), pair_value (val1,val2)= let sto=update_variable (sto，var1,val1) in update_variable (sto,var2,val2) 添加識(shí)別(identify)和分配變量存儲(chǔ)(allocate_variable)的語義

37、函數(shù)：identify: V-name (Environ Value_or_Variable)Value_or_Variable = value Value + variable Variable identifyI env = find(env，I) identifyfst V env = let first (value (pair_value (val1，val2) = value val1 first (variable (pair_variable (var1，var2) = variable var1 in first (identify V env)/輔助函數(shù)first將對(duì)偶值或

38、對(duì)偶變量映射為它的第一子域。賦值語句語義等式：execute V:= E env sto = let val = evaluate E env sto in let variable var = identify V env in update_variable (sto，var，val)evaluate V env sto= coerce (sto，identify V env)coerce: Store Value_or_VariableValue coerce (sto，value val ) = val coerce (sto，variable var) = fetch_variabl

39、e (sto，var) allocate_variable: Type_denoterAllocatorAllocator = Store StoreVariable 例：為類型指明符bool分配存儲(chǔ)的語義是: allocate_variable bool sto= let (sto，loc) = allocate sto in (sto，simple_variable loc)為對(duì)偶指明符分配存儲(chǔ)的語義是: allocate_variable(T1，T2) sto= let (sto，var1) = allocate_variable T1 sto in let (sto，var2) = a

40、llocate_variable T2 sto in (sto，pair_variable (var1，var2)變量聲明的語義: elaboratevar I:T env sto= let (sto，var) = allocate_variable T sto in (bind(I，var)，sto)數(shù)組變量的語義描畫(參考教材)16.5 16.5 程序失敗的語義描畫程序失敗的語義描畫sum: Integer sum: Integer Integer Integer Integer Integer sum (int1 sum (int1，int2) = if abs(int1+int2) =

41、maxintint2) = if abs(int1+int2) =maxint then int1+int2 then int1+int2 else else sum ( sum (，int2)= int2)= sum (int1 sum (int1，) = ) = evaluate evaluate E1 + E2E1 + E2 env sto = env sto = let integer int1 = evaluate E1 env sto in let integer int1 = evaluate E1 env sto in let integer int2 = evaluete E

42、2 env sto in let integer int2 = evaluete E2 env sto in integer (sum (int1 integer (sum (int1，int2)int2)16.6 16.6 指稱語義運(yùn)用指稱語義運(yùn)用 指稱語義用于設(shè)計(jì)言語指稱語義用于設(shè)計(jì)言語 為一個(gè)程序設(shè)計(jì)言語寫指稱語義的步驟是為一個(gè)程序設(shè)計(jì)言語寫指稱語義的步驟是: :分析分析( (所設(shè)計(jì)的所設(shè)計(jì)的) )程序設(shè)計(jì)言語的規(guī)格闡明寫出籠統(tǒng)語法。程序設(shè)計(jì)言語的規(guī)格闡明寫出籠統(tǒng)語法。定義該言語的指稱域，并為這些域定義洽當(dāng)?shù)妮o助函數(shù)以模定義該言語的指稱域，并為這些域定義洽當(dāng)?shù)妮o助函數(shù)以模型值上的操作。型

43、值上的操作。 建立語義函數(shù)。為籠統(tǒng)語法中的每個(gè)短語建立語義函數(shù)。為籠統(tǒng)語法中的每個(gè)短語( (即短語類即短語類) )指定一指定一個(gè)域個(gè)域( (語義函數(shù)的語義函數(shù)的 輸入域輸入域) )，定義輸入域到其指稱域的語義函，定義輸入域到其指稱域的語義函數(shù)。數(shù)。為每一短語類寫出語義等式。為每一短語類寫出語義等式。16.6.2 16.6.2 指稱語義用于程序性質(zhì)研討指稱語義用于程序性質(zhì)研討 上下文約束的靜態(tài)描畫上下文約束的靜態(tài)描畫在程序設(shè)計(jì)言語的文法產(chǎn)生的一切句子之中只需一部分在程序設(shè)計(jì)言語的文法產(chǎn)生的一切句子之中只需一部分是良定義的。語法往往不能給出明確的表示，要依托上是良定義的。語法往往不能給出明確的表示

44、，要依托上下文約束。下文約束。用指稱語義的方法描畫程序設(shè)計(jì)言語的上下文約束要建用指稱語義的方法描畫程序設(shè)計(jì)言語的上下文約束要建立類型環(huán)境的概念。言語中各類型之總稱即為立類型環(huán)境的概念。言語中各類型之總稱即為TypeType域。域。例如，在前述例如，在前述IMPIMP言語中類型域是言語中類型域是: :Type=truth_type + integer_type + var_type + Type=truth_type + integer_type + var_type + error_type error_type Type_Environ = Identifier(bound Type + u

45、nbound) Type_Environ = Identifier(bound Type + unbound) equivalent: Typeequivalent: TypeTypeTruth_Value TypeTruth_Value 可測(cè)試兩種類型能否等價(jià)。 constrain: Command(Type_EnvironTruth_Value) 檢查命令在類型環(huán)境中能否服從約束，即能否良定義的。 typify: Expression(Type_EnvironValue_Type) 驗(yàn)明表達(dá)式的類型，即在類型環(huán)境中的詳細(xì)類型。 declare : Declaration(Type_Envi

46、ronTruth_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。要證明相等，即指出兩端指稱一樣即可

47、: 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;再寫出詳細(xì)函數(shù)定義:fun execute (skip) env sto = sto e

48、xecute (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 16.6.3 語義原型語義原型先將籠統(tǒng)語法改寫為先將籠統(tǒng)語法改寫為MLML的的data

49、type datatype 定義定義: : type Identifier = string type Identifier = string and Num eral = string; and Num eral = string; datatype Command = datatype Command = skip skip IbecomesE of Identifier IbecomesE of Identifier * * Expression Expression letDinC of Declaraton letDinC of Declaraton * * Command Comm

50、and CsemicolonC of Command CsemicolonC of Command * * Command Command ifEthenCelseC of Expressiion ifEthenCelseC of Expressiion * * Command Command * * Command Command whileEdoC of Expression whileEdoC of Expression * * Command Command and Expression = and Expression = num of Numeral num of Numeral

51、flaseflase truetrue ide of Identifieride of Identifier EplusE of Expression EplusE of Expression * * Expression Expression and Declaration= and Declaration= constIisE of Ldentifier constIisE of Ldentifier * * Expression Expression varIcolonT of LdentifiervarIcolonT of Ldentifier* * Typerdenoter Typerdenoter and Typedenoter= and Typedenoter= bool bool intint將域的各等