Часть II. Формальное описание языков программирования ( Формальная спецификация формальных языков ) Приложение. Описание статической семантики языка IMP в форме wf-функций

Программа type Type_id = int | bool | fun, Id= Text Env :: vars : Id –m-> Type_id, funs : Id –m-> Parm-list -- Prog :: Block is_wf_Prog : Prog -> Bool is_wf_Prog (b) is is_wf_Block(b, )

Блок (декларации) -- Block :: Decl-list Stmt-list is_wf_Block (mk_Block(dl, sl),envl) is local variable locenv = Env := [ ], wf = Bool := true, i = Nat := 0 in i:= 1; while i inds dl wf do if is_wf_Decl (dl(i), locenv ^ envl) then i := i + 1; locenv := addDecl(dl(i),locenv) else wf := false end end;

Блок (операторы) i:= 1; while i inds sl wf do if is_wf_Stmt (sl(i), locenv ^ envl) then i := i + 1 else wf := false end end; wf end

Декларации -- Decl = Var_Def Func_Def is_wf_Decl : Decl -> Bool is_wf_Decl (d, env) is case d of Var_Def (_) -> is_wf_Var_Def(d,envl), Func_Def(_) -> is_wf_Def(d,envl) end

Декларации переменных -- Var_Def :: Id Type_Desc is_wf_ Var_Def : Var_Def Env-list-> Bool is_wf_ Var_Def (mk_Var_Def(id,typedesc), envl) is id unionVarsDom (envl) id unionFunsDom (envl) ((typedesc = int) (typedesc = bool))

Декларации функций -- Fun_Def :: Id Param-list Type_Desc Block is_wf_ Fun_Def : Fun_Def Env-list-> Bool is_wf_ Fun_Def (mk_Fun_Def(id, pl, typedesc, bk), envl) is id unionVarsDom (envl) id unionFunsDom (envl) (typedesc = int) local variable locenv = Env := [ ], wf = Bool := true, i = Nat := 0 in i:= 1; while i inds pl wf do if is_wf_Param (pl(i), locenv) then i := i + 1; locenv := addDecl(pl(i),locenv) else wf := false end end; wf is_wf_Block (bk, locenv ^ envl)

Формальные параметры -- Param :: Id Type_Desc is_wf_Param : Param Env -> Bool is_wf_Param (mk_Param(id, Type_Desc), env) is id dom env ((typedesc = int) (typedesc = bool))

Операторы -- Stmt = Assign Block If While is_wf_Stmt : Stmt Env-list -> Bool is_wf_Stmt (s, envl) is case s of mk_Assing (_, _) -> is_wf_Assing(s,envl), mk_Block(_, _) -> is_wf_Block(s,envl), mk_If (_) -> is_wf_If(s,envl), mk_While(_, _) -> is_wf_While(s, envl) end

Оператор присваивания -- Assign :: Id Expr is_wf_Assing : Assing Env-list -> Bool is_wf_Assing (mk_Assing(id, expr), envl) is is_wf_Expr(expr, envl) if id unionFunsDom(envl)then case expr of mk_Intexp (_) -> true, _ -> false end elsif id unionVarsDom(envl)then case expr of mk_Intexp (_) -> mapVarsDom(id, envl) = int, mk_Boolexp(_) -> mapVarsDom(id, envl) = bool end

Оператор If -- If = If_pair-list is_wf_If : If Env-list -> Bool is_wf_If (ifl, envl) is local wf = Bool := true in forall i isin inds ifl do let mk_if_pair(c,s) = ifl(i) in wf := wf is_wf_Boolexp(c, hd envl) is_wf_Stmts(s, hd envl) end end; wf end len ifl > 1 let mk_Boolexp(c, _) = ifl(len ifl) in c = True end end

Оператор While -- While :: Boolexp Stmt-list is_wf_While : While Env-list -> Bool is_wf_While (mk_While(c, sl), envl) is local wf = Bool := true in is_wf_Boolexp(c, envl) forall i isin inds sl do wf := wf is_wf_Stmts(sl(i), envl) end; wf end

Выражения -- Expr = Intexp Boolexp is_wf_Expr : Expr Env-list -> Bool is_wf_Expr (e, envl) is case s of mk_Intexp (_) -> is_wf_Intexp(e,envl), mk_Boolexp(_) -> is_wf_Boolexp(e,envl) end

Арифметические выражения -- Intexp = Integer Id Bi_Int_Exp Funcall is_wf_Intexp : Intexp Env-list -> Bool is_wf_Intexp (e, envl) is case s of mk_Integer (_) -> true, mk_Id(_) -> unionVarsDom(envl) mapVarsDom(id, envl) = int, mk_Bi_Int_Exp (_) -> is_wf_Bi_Int_Exp(e,envl), mk_Funcall (_) -> is_wf_Funcall(e,envl) end

Булевские выражения -- Boolexp :: False | True | Id | Equal | Comp is_wf_Boolexp : Boolexp Env-list -> Bool is_wf_Boolexp (e, envl) is case s of False -> true, True -> true, mk_Id (_) -> unionVarsDom(envl) mapVarsDom(id, envl) = bool mk_Equal(_) -> is_wf_Equal(e,envl), mk_Comp(_) -> is_wf_Comp(e, envl) end

Выражение = -- Equal :: Expr Expr is_wf_ Equal : Equal Env-list -> Bool is_wf_ Equal (mk_ Equal(left, right), envl) is is_wf_Expr(left,envl) is_wf_Expr(right,envl) end

Выражения >, < -- Comp :: Intexp Comp_Op Intexp is_wf_ Comp : Comp Env-list -> Bool is_wf_ Comp (mk_ Equal(left, _, right), envl) is is_wf_Intexp(left,envl) is_wf_Intexp(right,envl) -- Comp_Op = Greater Less

Бинарные арифметические выражения -- Bi_Int_Exp :: Int_Exp Ar_Operation Int_Expr is_wf_Bi_Int_Exp : Bi_Int_Exp Env-list -> Bool is_wf_ Bi_Int_Exp (mk_ Bi_Int_Exp(left, _, right), envl) is is_wf_Bi_Int_Exp(e,envl)

Вызов функции (Function Call) -- Funcall ::= Id Arg-list is_wf_ Funcall : Funcall Env-list -> Bool is_wf_ Funcall (mk_ Funcall(id, argl), envl) is id unionFunsDom (envl) local wf = Bool := true in forall i isin inds argl do wf := wf is_wf_Expr(argl(i), envl) case argl(i) of mk_Intexp (_) -> unionMapFuns(id, envl)(i) = int, mk_Boolexp(_) -> unionMapFuns(id, envl)(i) = bool end; wf end