(a)
Routine credit (amount) is public
   Slot amount ofType real
-- Does deposit an amount into account
    PreCheck (amount >= 0.00) bounce "Negative deposit!"

(b)
PreCheck (amount >= 0.00) bounce "Negative deposit!"

(c)
if (amount >= 0.00) JJSystem.halt("Negative deposit!");

Example 2: JJ preconditions and postconditions.