代数语义学

代数语义学内容摘要：

程序抽象的语义描述 函数抽象 Function = Argument→Value Function = Argument→Store→Value bind_parameter: Formal_Parameter→(Argument→Environ) give_argument : Actual_Parameter→(Environ→Argument) 扩充 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函数的指称语义 bindparameter 〖 I:T〗 arg = bind (I， arg) giveargument 〖 E〗 env = evaluate E env 函数调用的语义等式如下 : 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) 参数机制的语义描述 常量和变量参数 先细化参数定义语法 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) 实参的语义等式是 : 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 复制参数机制 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) 多参数 Function = Argument*→Store→Value Procedure = Argument* →Store→Store bind_parameter : Formal_Parameter_List→(Argument * →Environ) give_argument:Acrual_Parameter_List→(Environ →Store →Argament *) 递归抽象 递归函数声明的语义等式如下 : 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。 ))。