context PayCard 
  inv withinLimit : balance >= 0 and balance <= limit