function after_tax
    (before_tax: Natural;
     rate      : Natural) return Natural
with
   Pre  => (rate <= 100),
   Post => (after_tax'result  <= before_tax);