• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Riscv
      • Taspi
      • Bitcoin
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Aleo
        • Aleobft
        • Aleovm
        • Leo
          • Grammar
          • Early-version
            • Json2ast
            • Testing
            • Definition
              • Flattening
              • Abstract-syntax
              • Dynamic-semantics
                • Execution
                  • Exec-expressions/statements
                  • Init-for-loop
                  • Exec-file-main
                  • Update-variable-value-in-scope-list
                  • Step-for-loop
                  • Update-variable-value-in-scope
                  • Expr-value-to-value
                  • Exec-binary
                  • Exec-expression
                  • Init-vcscope-dinfo-call
                  • Value?+denv
                  • Exec-statement
                    • End-of-for-loop-p
                    • Expr-value
                    • Evalue+denv
                    • Write-location
                    • Read-location
                    • Exec-for-loop-iterations
                    • Update-variable-value
                    • Exec-unary
                    • Values+denv
                    • Init-vcscope-dinfo-loop
                    • Extend-denv-with-structdecl
                    • Exec-var/const
                    • Valuemap+denv
                    • Namevalue+denv
                    • Extend-denv-with-fundecl
                    • Ensure-boolean
                    • Int+denv
                    • Push-vcscope-dinfo
                    • Extend-denv-with-topdecl-list
                    • Exec-literal
                    • Build-denv-from-file
                    • Namevalue+denv-result
                    • Extend-denv-with-topdecl
                    • Evalue+denv-result
                    • Value?+denv-result
                    • Values+denv-result
                    • Valuemap+denv-result
                    • Int+denv-result
                    • Push-call-dinfo
                    • Exec-print
                    • Pop-vcscope-dinfo
                    • Exec-if
                    • Exec-function
                    • Pop-call-dinfo
                    • Exec-statement-list
                    • Exec-block
                    • Exec-struct-init-list
                    • Exec-struct-init
                    • Exec-expression-list
                  • Values
                  • Dynamic-environments
                  • Arithmetic-operations
                  • Curve-parameterization
                  • Shift-operations
                  • Errors
                  • Value-expressions
                  • Locations
                  • Input-execution
                  • Edwards-bls12-generator
                  • Equality-operations
                  • Logical-operations
                  • Program-execution
                  • Ordering-operations
                  • Bitwise-operations
                  • Literal-evaluation
                  • Type-maps-for-struct-components
                  • Output-execution
                  • Tuple-operations
                  • Struct-operations
                • Compilation
                • Static-semantics
                • Concrete-syntax
        • Bigmems
        • Builtins
        • Execloader
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Community
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Execution
    • Exec-expressions/statements

    Exec-statement

    Execute a statement.

    Signature
    (exec-statement stmt env limit) → value?+denv
    Arguments
    stmt — Guard (statementp stmt).
    env — Guard (denvp env).
    limit — Guard (natp limit).
    Returns
    value?+denv — Type (value?+denv-resultp value?+denv).

    A variable or constant declaration is executed by first evaluating the initializing expression, then ensuring that it has the type of the variable or constant, and finally adding it to the environment. We return no value.

    For an assignment, we evaluate both expressions, ensuring that the first one returns a location. We update the location with a value, which also ensures that the new value has the same type as the old value. We return no value

    For a return statement, we evaluate the expression, and return its value as the return value of the statement.

    For a loop statement, we first evaluate the starting and ending exxpressions. Then we initialize the loop, via init-for-loop, by adding a scope with the loop counter and obtaining the loop bound (i.e. the ending value). The loop iterations are executed by exec-for-loop-iterations.

    A console assertion statement is executed by evaluating the expression, and ensuring that it is a boolean. If the boolean is false, we stop with an assertion error. Otherwise we proceed: a console assertion statement returns no value.

    A console print statement is executed by evaluating the expressions, and then printing the message on the screen. This kind of statement returns no value.