------------------------------------------------------------------------

Modeling versus Programming

- assume a simple, naive software development cycle:
  requirements, design, implementation, maintenance

- models: typically employed within requirements and design

- models: formulation of desired system properties independent from a
  particular implementation or platform

- models: analysis of properties like consistency, reachability,
  absense of contradictions

- programs: typically with the implementation phase

- programs: efficient execution in a special programming language

- transformation: model to program; conservation of properties as
  correctness; object-oriented model not neccessarily implemented in
  an object-oriented programming language

- e.g.: different programming languages / platforms for smart phone
  apps; model to implementation-1, ..., implementation-n

------------------------------------------------------------------------

model = (here) UML model (Unified Modeling Language)

- class diagrams with classes, attributes, operations, associations;
  aggregation, composition, generalization, association classes,
  derived elements, ...; statechart diagrams; ...

- OCL constraints (Object Constraint Language); restrictions to make
  the diagrams more precise; e.g. class invariants, operation pre- and
  postconditions

- invariants: valid within a class when no operation is active;
  preconditions: valid before an operation call; postconditions: valid
  after operation execution; pre- and postconditions: design-by-contract

- structure: concentrating on classes and associations (and further
  elements)

- behavior: operations; pre- postconditions; statecharts

- validation: are we building the right product? model versus informal
  requirements

- verification: are we building the product right? detection of
  properties of the model and its correctness with regard to the
  implementation

- validation in USE (UML-based Specification Environment): with 
  scenarios; object, sequence, communication diagrams

- verification in USE: (semi-automatic) construction of object,
  sequence, communication diagrams with particular
  properties

------------------------------------------------------------------------

examples: marriage model in 'USE 4 EIS'

- validation

  association Marriage between
    Person [0..1] role wife
    Person [0..1] role husband
   end

  context: historical information about marriages between *Mormon*
  people has to be modeled

  multiplicity '[0..1] role wife' should not be validated, because at
  least one scenario should be present in which one male person is
  connected to two wifes

- verification

  Is this model bigamy free? is the following OCL formula valid?

  not Person.allInstances->exists(p |
    p.wife->notEmpty and p.husband->notEmpty)

  the considered Marriage model is bigamy free, because in the above
  OCL formula the person p is occurring in the the role wife *and* in
  the role husband; however, a male person is not allowed to have a
  husband according to one invariant, a female person is not allowed
  to have a wife according to another invariant, and the attribute
  gender is not allowed to be undefined according to a third invariant

------------------------------------------------------------------------