diff options
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/julia.rst | 154 |
1 files changed, 87 insertions, 67 deletions
diff --git a/docs/julia.rst b/docs/julia.rst index 8812bab2..9f098880 100644 --- a/docs/julia.rst +++ b/docs/julia.rst @@ -89,7 +89,7 @@ Grammar:: Expression = FunctionCall | Identifier | Literal Switch = - 'switch' Expression Case+ ( 'default' Block )? + 'switch' Expression Case* ( 'default' Block )? Case = 'case' Literal Block ForLoop = @@ -116,134 +116,154 @@ Grammar:: Restrictions on the Grammar --------------------------- -Scopes in JULIA are tied to Blocks (exceptions are functions and the for loop) and all declarations -(``FunctionDefinition``, ``VariableDeclaration``) -introduce new identifiers into these scopes. Identifiers are visible in -the block they are defined in (including all sub-nodes and sub-blocks). -Shadowing is disallowed, i.e. you cannot declare an identifier at a point -where another identifier with the same name is also visible. - -Switches must have at least one (or the default) and at most one default case. +Switches must have at least one case (including the default case). If all possible values of the expression is covered, the default case should not be allowed (i.e. a switch with a ``bool`` expression and having both a true and false case should not allow a default case). -In for-loops, identifiers declared in the first block (the init block) -are visible in all other parts of the for loop (but not outside of the loop). -Identifiers declared in the other parts of the for loop respect the regular -syntatical scoping rules. - -Inside functions, it is not possible to access a variable that was declared -outside of that function. - -Every expression evaluates to zero or more values. Literals evaluate to exactly +Every expression evaluates to zero or more values. Identifiers and Literals +evaluate to exactly one value and function calls evaluate to a number of values equal to the -number of return values of the function called. An expression that is also -a statement is invalid if it evaluates to more than one value, i.e. at the -block-level, only expressions evaluating to zero values are allowed. +number of return values of the function called. -For variable declarations and assignments, the right-hand-side expression +In variable declarations and assignments, the right-hand-side expression (if present) has to evaluate to a number of values equal to the number of variables on the left-hand-side. +This is the only situation where an expression evaluating +to more than one value is allowed. -An expression used as an argument to a function call has to evaluate to exactly -one value. +Expressions that are also statements (i.e. at the block level) have to +evaluate to zero values. -The ``continue`` and ``break`` statements can only be used inside loop bodies. +In all other situations, expressions have to evaluate to exactly one value. + +The ``continue`` and ``break`` statements can only be used inside loop bodies +and have to be in the same function as the loop (or both have to be at the +top level). The condition part of the for-loop has to evaluate to exactly one value. Literals cannot be larger than the their type. The largest type defined is 256-bit wide. +Scoping Rules +------------- + +Scopes in JULIA are tied to Blocks (exceptions are functions and the for loop +as explained below) and all declarations +(``FunctionDefinition``, ``VariableDeclaration``) +introduce new identifiers into these scopes. + +Identifiers are visible in +the block they are defined in (including all sub-nodes and sub-blocks). +As an exception, identifiers defined in the "init" part of the for-loop +(the first block) are visible in all other parts of the for-loop +(but not outside of the loop). +Identifiers declared in the other parts of the for loop respect the regular +syntatical scoping rules. +The parameters and return parameters of functions are visible in the +function body and their names cannot overlap. + +Variables can only be referenced after their declaration. In particular, +variables cannot be referenced in the right hand side of their own variable +declaration. +Functions can be referenced already before their declaration (if they are visible). + +Shadowing is disallowed, i.e. you cannot declare an identifier at a point +where another identifier with the same name is also visible, even if it is +not accessible. + +Inside functions, it is not possible to access a variable that was declared +outside of that function. + Formal Specification -------------------- We formally specify JULIA by providing an evaluation function E overloaded on the various nodes of the AST. Any functions can have side effects, so -E takes a state objects and the actual argument and also returns new -state objects and new arguments. There is a global state object +E takes two state objects and the AST node and returns two new +state objects and a variable number of other values. +The two state objects are the global state object (which in the context of the EVM is the memory, storage and state of the -blockchain) and a local state object (the state of local variables, i.e. a +blockchain) and the local state object (the state of local variables, i.e. a segment of the stack in the EVM). +If the AST node is a statement, E returns the two state objects and a "mode", +which is used for the ``break`` and ``continue`` statements. +If the AST node is an expression, E returns the two state objects and +as many values as the expression evaluates to. -The evaluation function E takes a global state, a local state and -a node of the AST and returns a new global state, a new local state -and a variable number of values. The exact nature of the global state is unspecified for this high level -description. The local state `L` is a mapping of identifiers `i` to values `v`, -denoted as `L[i] = v`. -The special value `⊥` is used to signify that a variable cannot be -used yet. +description. The local state ``L`` is a mapping of identifiers ``i`` to values ``v``, +denoted as ``L[i] = v``. + +For an identifier ``v``, let ``$v`` be the name of the identifier. + +We will use a destructuring notation for the AST nodes. .. code:: E(G, L, <{St1, ..., Stn}>: Block) = - let L' be an extension of L to all variables v declared in Block - (but not in its sub-blocks), such that L'[v] = ⊥. - let Gi, Li, mode = E(G, L', St1, ..., Stn) - let L'' be a restriction of Li to the identifiers of L - Gi, L'', mode + let G1, L1, mode = E(G, L, St1, ..., Stn) + let L2 be a restriction of L1 to the identifiers of L + G1, L2, mode E(G, L, St1, ..., Stn: Statement) = if n is zero: G, L else: - let G', L', mode = E(G, L, St1) + let G1, L1, mode = E(G, L, St1) if mode is regular then - E(G', L', St2, ..., Stn) + E(G1, L1, St2, ..., Stn) otherwise - G', L', mode - E(G, L, <function fname (param1, ..., paramn) -> (ret1, ..., retm) block>: FunctionDefinition) = + G1, L1, mode + E(G, L, FunctionDefinition) = G, L, regular E(G, L, <let var1, ..., varn := rhs>: VariableDeclaration) = E(G, L, <var1, ..., varn := rhs>: Assignment) E(G, L, <let var1, ..., varn>: VariableDeclaration) = - let L' be a copy of L where L'[vi] = 0 for i = 1, ..., n - G, L', regular + let L1 be a copy of L where L1[$vari] = 0 for i = 1, ..., n + G, L1, regular E(G, L, <var1, ..., varn := rhs>: Assignment) = - let G', L', v1, ..., vn = E(G, L, rhs) - let L'' be a copy of L' where L'[vi] = vi for i = 1, ..., n - G, L'', regular + let G1, L1, v1, ..., vn = E(G, L, rhs) + let L2 be a copy of L1 where L2[$vari] = vi for i = 1, ..., n + G, L2, regular E(G, L, <for { i1, ..., in } condition post body>: ForLoop) = if n >= 1: - let L' be an extension of L to all variables v declared in i1, ..., in - (but not in sub-blocks), such that L'[v] = ⊥. - let G'', L'', mode = E(G, L', i1, ..., in) - explode if mode is not regular - let G''', L''', mode = E(G'', L'', for {} condition post body) - explode if mode is not regular - let Lend be the restriction of L''' to only variables of L - G''', Lend + let G1, L1, mode = E(G, L, i1, ..., in) + // mode has to be regular due to the syntactic restrictions + let G2, L2, mode = E(G1, L1, for {} condition post body) + // mode has to be regular due to the syntactic restrictions + let L3 be the restriction of L2 to only variables of L + G2, L3 else: - let G', L', v = E(G, L, condition) + let G1, L1, v = E(G, L, condition) if v is false: - G', L', regular + G1, L1, regular else: - let G'', L'', mode = E(G, L, body) + let G2, L2, mode = E(G1, L, body) if mode is break: - G'', L'', regular + G2, L2, regular else: - G''', L''', mode = E(G'', L'', post) - E(G''', L''', for {} condition post body) + G3, L3, mode = E(G2, L2, post) + E(G3, L3, for {} condition post body) E(G, L, break: BreakContinue) = G, L, break E(G, L, continue: BreakContinue) = G, L, continue E(G, L, <name>: Identifier) = - G, L, regular, L[name] + G, L, regular, L[$name] E(G, L, <fname(arg1, ..., argn)>: FunctionCall) = G1, L1, vn = E(G, L, argn) ... G(n-1), L(n-1), v2 = E(G(n-2), L(n-2), arg2) Gn, Ln, v1 = E(G(n-1), L(n-1), arg1) Let <function fname (param1, ..., paramn) -> ret1, ..., retm block> - be the function of name fname visible at the point of the call. + be the function of name $fname visible at the point of the call. Let L' be a new local state such that - L'[parami] = vi and L'[reti] = 0 for all i. + L'[$parami] = vi and L'[$reti] = 0 for all i. Let G'', L'', rv1, ..., rvm = E(Gn, L', block) G'', Ln, rv1, ..., rvm E(G, L, l: HexLiteral) = G, L, hexString(l), - where hexString decodes l from hex and left-aligns in into 32 bytes + where hexString decodes l from hex and left-aligns it into 32 bytes E(G, L, l: StringLiteral) = G, L, utf8EncodeLeftAligned(l), where utf8EncodeLeftAligned performs a utf8 encoding of l and aligns it left into 32 bytes |