We want to define the memory consumption of an IMP- program over its execution, and give an upper bound that is based on the number of steps the program is executed for, the number of registers that are used in the program, the maximal constant that appears in the program and the initial values of these registers.
We imagine that we define memory(c, s) = max_t Sum_i log_2 r_{i, t}' , wherec' is an IMP-- program, s' is the initial state, andr_{i,t}' is the value of register r_i' after executingt' steps.
We then should be able to show that if c' terminates ons' after at most t steps, then memory(c, s) <= t + num_registers_in_c * (max {max_constant(c), max_i (s r_i)})
We want to define the memory consumption of an IMP- program over its execution, and give an upper bound that is based on the number of steps the program is executed for, the number of registers that are used in the program, the maximal constant that appears in the program and the initial values of these registers.
We imagine that we define
memory(c, s) = max_t Sum_i log_2 r_{i, t}' , wherec' is an IMP-- program,s' is the initial state, andr_{i,t}' is the value of registerr_i' after executingt' steps.We then should be able to show that if
c' terminates ons' after at mosttsteps, thenmemory(c, s) <= t + num_registers_in_c * (max {max_constant(c), max_i (s r_i)})