A process and a system are used to verify that an object-oriented software component described in an extended programming language behaves correctly with respect to an abstract data model and specifications of the operations that may be performed on it The process and system also verify for an assembly of components that whenever an operation on a component is invoked, the correct conditions specified for that operation and component exist, and that specified properties hold for a component of the assembly.