Claim: if we apply translation above then the stack size at each point in the bytecode can be computed during compilation.

• we can check for stack underflow and overflow

Why does it hold?

• for each assignment statement
• for if, while

Can JVM rely on this property?

• what if bytecode is not compiled from java / tool ?
• bytecode verifier checks the stack usage (including stack depth and initialization)

Consider depth computation for Compiled Factorial Example

How does this property relate to Translation Correctness for Expressions?

• the property implies that compilation of expression only adds one value to the stack in the end
• assignment will consume this value, so each assignment leaves stack unchanged!