! proclang.txt - example procedural langauge definition ! (see SIGPLAN [82] for original version) ! example function defined in a simple Ada-like procedural language: (function FACTORIAL (N) is variables I FACT ; ! list of local variable names begin ! arguments & local variables are untyped I := 0 ; FACT := 1 ; ! = 0! = I! while I < N loop ! loop until I = N I := I + 1 ; FACT := FACT * I ; ! FACT := I! end loop ; end FACTORIAL return FACT). ! since I = N, FACT = N! !/ This unconditional axiom, combined with axioms below that define this procedural language, generate valid expressions such as, (FACTORIAL (`s `s `s `0) (`s `s `s `s `s `s `0)) -- 3! = 6 which define the factorial function. !\ ! top-level axiom for this language (%fname \$argvals %result)< ! function to be defined (function %fname (\$argnames) is ! procedural lang expr variables \$locnames ; ! local variable names begin \$stmts ! algorithm statements end %fname return \$result_expr), ! result of function (=length (\$argnames) (\$argvals)), ! pair arg names & values (exec (\$stmts) (\$argnames \$locnames) (\$argvals \$dummy) %finalvals), (expr (\$result_expr) (\$argnames \$locnames) %finalvals %result). ! exec - execution of a statement sequence ! (exec ) ! grammar: ! Stmts = | S ; Stmts ! S = V := E -- assignment statement ! S = while Bool loop Stmts end loop -- while loop (exec () %vars %vals %vals). ! null sequence of statements (exec (\$S ; \$Stmts) %vars %vals %vals')< ! non-null statement sequence (execS (\$S) %vars %vals %valsx), (exec (\$Stmts) %vars %valsx %vals'). ! execS -- S = Name := Expr -- assignment statement (execS (%name := \$expr) (\$n1 %name \$n2) (\$v1 %val \$v2) (\$v1 %val' \$v2))< (=length (\$n1) (\$v1)), ! original value is replaced with val' (expr (\$expr) (\$n1 %name \$n2) (\$v1 %val \$v2) %val'). ! evaluate expr ! execS -- S = while B loop Stmts end loop -- while loop (execS (while \$B loop \$Stmts end loop) %names %vals %vals)< (exprB (\$B) %names %vals `false). ! Boolean false -- loop 0 times (execS (while \$cond loop \$Stmts end loop) %names %vals %vals')< (exprB (\$B) %names %vals `true), ! Boolean condition true (exec (\$Stmts) %names %vals %valsx), ! loop 1 or more times (execS (while \$B loop \$Stmts end loop) %names %valsx %vals'). ! expr -- Expr = E | B -- expression is numeric or Boolean ! (expr ) (expr (\$exprE) %names %vals %result)< (exprE (\$exprE) %names %vals %result). ! numeric expr (expr (\$exprB) %names %vals %result)< (exprB (\$exprB) %names %vals %result). ! Boolean expr ! exprE -- E = T | E + T -- numeric Expression ! -- numeric expression yields natural number result (exprE (\$exprT) %names %vals %result)< ! E = T (exprT (\$exprT) %names %vals %result). (exprE (\$exprE + \$exprT) %names %vals %result)< ! E = E + T (exprE (\$exprE) %names %vals %resultE), (exprT (\$exprT) %names %vals %resultT), (`plus %resultE %resultT %result). ! exprT -- T = P | T * P -- numeric Term (exprT (\$exprP) %names %vals %result)< ! T = P (exprP (\$exprP) %names %vals %result). (exprT (\$exprT * \$exprP) %names %vals %result)< ! T = T * P (exprT (\$exprT) %names %vals %resultT), (exprP (\$exprP) %names %vals %resultP), (`times %resultT %resultP %result). ! exprP -- P = num | name | ( E ) -- numeric primary (exprP (%decnum) %names %vals %num)< ! P = num (decnum %decnum %num). ! decimal symbol > natural number (exprP (%name) (\$n1 %name \$n2) (\$v1 %val \$v2) %val)< ! P = name (=length (\$n1) (\$v1). (exprP ((\$exprE)) %names %vals %result)< ! P = ( E ) (exprE (\$exprE) %names %vals %result). ! Boolean expr -- B = BC | BD -- conjunction or disjunction ! -- Boolean expression evaluates to atom `true or `false ! -- note that we can't write "x and y or z" -- must use parentheses! (exprB (\$exprB) %names %vals %result)< ! B = BC (one_valid ! higher-order form! (exprBC (\$exprB) %names %vals %result) (exprBD (\$exprB) %names %vals %result)). ! exprBC -- BC = BP | BC and BP -- Boolean conjunction (exprBC (\$BP) %names %vals %result)< ! BC = BP (exprBP (%BP) %names %vals %result). (exprBC (\$BC and \$BP) %names %vals %result)< ! BC = BC and BP (exprBC (\$BC) %names %vals %resultBC), (exprBP (\$BP) %names %vals %resultBP), (`and %resultBC %resultBP %result). ! exprBD -- BD = BP | BD and BP -- Boolean disjunction (exprBD (\$BP) %names %vals %result)< ! BD = BP (exprBP (%BP) %names %vals %result). (exprBD (\$BD or \$BP) %names %vals %result)< ! BD = BD or BP (exprBD (\$BD) %names %vals %resultBD), (exprBP (\$BP) %names %vals %resultBP), (`or %resultBD %resultBP %result). ! BP = `true | `false | | E E | ( B ) -- Boolean primary (exprBP (`true) %names %vals `true). ! BP = `true (exprBP (`false) %names %vals `false). ! BP = `false (exprBP (%name) (\$n1 %name \$n2) (\$v1 %val \$v2) %val)< ! BP = (=length (\$n1) (\$v1)). (exprBP (\$E1 %relop \$E2) %names %vals %result)< ! BP = E E (exprE (\$E1) %names %vals %num1), (exprE (\$E2) %names %vals %num2), (relop %relop %num1 %num2 %result). ! relational operator on numbers (exprBP ((\$B)) %names %vals %result)< ! BP = ( B ) (exprB (\$B) %names %vals %result). ! relop - relational operator on natural numbers (relop == %num %num `true)< (`number %num). (relop == %num1 %num2 `false)< (one_valid (