package Functions is
   function Multiply (A, B : Integer) return Integer;
   --# pre A * B in Integer; -- See note below
   --# return A * B; -- Implies commutativity on Multiply arguments
end Functions;