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;