An Executable Semantics of Object-oriented Models for Simulation and Theorem Proving