Samples Lists

Some examples We used Eclipse 2.1

Overview

File Description
Library This file is the example of the tutorial
Bank example based on banking operations
Company example based on the management of the employees
Component example based on a metamodel of component
Airport
 example based on airport modeling
  • Library
    library context Book
    inv: pages>0

    context Book
    inv: library.writers->includes(author)

  • Bank
    Bank context Account
    inv: balance>0

    context Account:output(money: int)
    pre: money>0
    post: balance=balance@pre-balance

    context Account
    inv: bank.customers->includes(owner)

  • Company
    Company context Company
    inv: self.manager.isUnemployed=false and self.manager.age>40 and self.employee-> notEmpty()

    context Person
    inv:
    let money: Real = self.job.salary-> sum() in
    if isUnemployed
    then money<100
    else money >= 100
    endif

    context Person::income() : Real
    post:
    if age<18
    then result=(parents.job.salary -> sum()) /100
    else result=self.job.salary -> sum()
    endif
  • Component

  • context Component
    inv: self.provides.forAll(p1, p2 | p1<>p2 implies p1.type<>p2.type)

    context Connection
    inv: self.from.type = self.to.type or self.to.type.getAllSupers() -> includes(self.from.type)

    context Connection
    inv: self.from.owner <> self.to.owner

    context Interface
    inv: not self.getAllSupers() -> includes(self)

    context Assembly
    inv: self.connections.forAll(c1,c2 | c1<>c2 implies c1.from <> c2.from)
  • Airport