Language "IBAFlang" Syntax START:start ::= pgm Semantics start[[ _:start ]] : =>null-type Rule start[[ Pgm ]] = initialise-binding finalise-failing run [[ Pgm ]] Syntax Pgm : pgm ::= 'int' idlist ';' stmt Semantics run[[ _:pgm ]] : =>null-type Rule run[[ 'int' IL ';' Stmt ]] = scope( collateral(declare-int-vars[[ IL ]]), execute[[ Stmt ]] ) Syntax IL : idlist ::= id (',' idlist)? Semantics declare-int-vars[[ _: idlist ]] : (=>environments)+ Rule declare-int-vars[[ Id ]] = bind(\"Id\", allocate-initialised-variable(integers, 0)) Rule declare-int-vars[[ Id ',' IL ]] = declare-int-vars[[ Id ]], declare-int-vars[[ IL ]] Lexis keyword ::= 'else' | 'false' | 'if' | 'true' | 'while' | 'int' Lexis SDF /* lexical syntax ``id`` = ``keyword`` {reject} lexical restrictions ``id`` -/- [A-Za-z0-9] */ Syntax SDF /* context-free syntax ``exp ::= exp '+' exp`` {assoc} ``exp ::= exp '&&' exp`` {assoc} ``stmt ::= stmt stmt`` {right} */