|
||||||||||
| PREV NEXT | FRAMES NO FRAMES | |||||||||
current contains ai, ..., an-1 with ai at the top of the stack
obj at the current position in the list.
obj at the current position in the list
Pre: #(L) = 0 or 0 <= i
Post: L' = #(L)+1
if #(L)=0 then i'=0, L' = (obj)
else if i>#(L)-1 then i' = #(L')-1, L' = (L, obj)
else i' = i, L' = (a0, ..., ai-1, obj, ai, ..., an-1)
Mapping: obj is pushed into the stack, current, on top of other objects in that stack
left contains a0, ..., ai-1 with ai-1 at the top of the stack
|
||||||||||
| PREV NEXT | FRAMES NO FRAMES | |||||||||