<b>(a)</b> Routine credit (amount) is public Slot amount ofType real -- Does deposit an amount into account PreCheck (amount >= 0.00) bounce "Negative deposit!" <b>(b)</b> PreCheck (amount >= 0.00) bounce "Negative deposit!" <b>(c)</b> if (amount >= 0.00) JJSystem.halt("Negative deposit!");
Example 2: JJ preconditions and postconditions.