shlaer-mellor-metamodel-verifier/doc/verifier-operation.txt

OOA domain model consists of:
   - object model (1)
   - state models (Mc)   <-]--Wouldn't be too interesting if both 0.
   - process models (Mc) <-]

Domain model must be verified per metamodel, which implies a verifier/parser of
whole model. Verifier probably is domain of metamodel.

Reporting domain must be a service provided to collect results of verification.

Precedence and AFAIK the only way of verifying is to convert model to some
text-based format.

Once the verifier has the model data it can:
   - Flag any unknown elements
   - Ensure all model construction rules are obeyed. e.g., when a relationship
     must have an associative object.
   - Formalize all relationships
   - Ensure user-defined types are mapped to a core type
      - NOTE: Might allow creation of new core types (???)
   - Verify process models with respect to:
      - data usage conforms to type
      - only supported operations are used
      - ensure all expressions conform to type usage
         - (???) type conversions
      - ensure all relationships are atomically satisfied on instance creation
      - ensure instances are created correctly
         - subtyping must specify whole branch
         - disallow static creation of objects with creation event

!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
NOTE: Definition objects can be constructed in the verifier for development
purposes to add some clarity, but they must be transformed into bridges in the
metamodel to ensure non-pollution!
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

Operation:
1. Collect and verify datatypes
   a. Establish new domain to be modeled
   b. Instantiate all core types.
2. Collect and verify new domain type operators
3. Collect and partially verify objects
   a. Verify non-referential attribute types
   b. Verify number of state models
      i. Only one instance state model
      ii. Only one assigner.
         A. Assigners are only allowed on associative objects.
   c. Identifier exists
   d. All attributes have a unique name.
4. Collect and verify relationships
   a. No duplicate relationship numbers
   b. Number of verb phrases.
      i. Reflexive can have one or two; all others have two.
   c. Multiplicity rules
      i. In cases where the model editing tool automatically adds the
         referential attributes, this checking could be disabled.
      ii. Association objects for M:M, Mc:M, Mc:Mc, 1c:M, and 1c:1c.
      iii. Referential attributes exist for each relationship.
         A. Two sets in association objects, else one set in involved objects.
         B. Set is on proper end of relationship.
            1. 1:1 either end
            2. 1c:1 on c end
            3. 1:M on M end
            4. Note that reflexive relationships will only involve one object.
   d. Ensure there are always two subtypes per supertype object.
5. Collect and verify accessors
   a. Verify parameter types
   b. Verify return types
   c. Ensure no returns on events.
   d. Ensure no duplicate accessor names within scope.
      i. Object-level names (events and object methods) in different objects 
         can be duplicates
      ii. Object-level names and non-object-level accessor names can be 
          duplicates
6. Collect process model translations
   a. Might have type-based operations. e.g., OAL uses '=' for assignment, but
      also supports create and assign statements, 'create object instance
      <varname>'.
7. Collect and verify all instantiations
   a. Instantiations occur on creation transitions or declaration of an
      instance variable.
   b. Ensure all unconditional relationships are satisfied within the atomic
      process that caused instantiation.
      i. No asynchronous calls occur before all unconditional relationships are
         satisfied.
      ii. Creation events atomicity is defined by entry state, but rule on
          self-directed events will allow satisfaction to span mutiple states.
   c. Identifying creations
      i. Instance creation
         A. requires an object reference
         B. doesn't require variable assignment Ex. <obj ref>[10] could create
            10 unassigned instances.
      ii. Event creation
         A. Should be identifiable from state model.
         B. Might have keyword.
         C. Doesn't participate in variable assignment. (asynchronous) 
         D. Creation state calls within the same state model are part of
            atomicity?

EXERCISING VERIFICATION TO BE DONE USING MICROWAVE OVEN
1. Creation starts with DOM, MDOM, R1
   a. NOTE: At this stage of the verification, there is no R105, so don't try to
      verify domain, until after at least one object is added!
2. Map core datatypes in OAL to metamodel
3. Then proceed from UDTs in sequence.
   a. Initial run-through with tube_wattage showed no unsatisfied unconditional
      relationships.
   b. Creation should be DOMD, TYPE, R401, R412, 5xENUV, 5xR404, 5xENUP, ENUD,
      5xR413, R416, 5xVAL, 5xDUS, 5xR629, 5xR624, 5xR625