【文章內(nèi)容簡介】 程序抽象的語義描述 函數(shù)抽象 Function = Argument→Value Function = Argument→Store→Value bind_parameter: Formal_Parameter→(Argument→Environ) give_argument : Actual_Parameter→(Environ→Argument) 擴(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ù)的指稱語義 bindparameter 〖 I:T〗 arg = bind (I， arg) giveargument 〖 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 = Argument→Store→Store 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 sto39。 = let parent = bindparameter FP arg in execute C (overlay (parenv env)) sto39。 in (bind (I， procedure proc)， sto) 參數(shù)機(jī)制的語義描述 常量和變量參數(shù) 先細(xì)化參數(shù)定義語法 FormalParameter ::= const Identifier: Type_denoter ｜ var Identifier : Type_denoter ActualP arameter ::= Expression ｜ var Identifier bind_parameter : Formal_parameter→(Argument→Environ) give_parameter : Actural_Parameter→(Environ→Store→Argument) 形參的語義等式是 : 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→(Argument→Store→Environ Store) copy_in 〖 value I:T〗 (value val) sto = let (sto39。， local) = allocate sto in (bind (I， variable local)， update (sto39。， local， val)) copyin 〖 result I:T〗 (variable loc) sto= let (sto39。， local)= allocate sto in (bind (I， variable local)， sto39。) copy_out: Formal_Parameter→(Environ→ Argument→Store→Store) 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)) 過程聲明的語義等式作以下修改 : elaborate〖 proc (FP) is C 〗 env sto= let proc arg sto39。= let (parenv， sto) copy_in FP arg sto39。 in let sto39。39。39。 = execute C (overlay (parenv， env )) sto in copy_out FP parenv arg sto39。39。39。 in (bind (I， procedure proc)， sto) 多參數(shù) Function = Argument*→Store→Value Procedure = Argument* →Store→Store 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 env39。=overlay (bind (I， function func)， env) in let parenv = bindparameter FP arg in evaluate E (overlay (parenv， env39。))