! 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 (