What is loop invariant for this loop?
"
    Pre: stack is empty or contains only integers
    Post: Stack top is non-negative Integer
    P:  Stack top is an Integer   ( P is the invariant )
    BB: Stack top is negative
    T:  Stack size
"

" Establish P "
stack size > 0 or: [stack push: 0].
[ stack top negative
] whileTrue:
    [ " reduce T "
      stack pop. 
      " restore P "
      stack size > 0 or: [stack push: 0]
    ]
" P && non BB => Post "