Classes

A class describes a part of the modeled system. Classes have state (variables), structure (features), and behavior (transitions, properties).

The Anything Base Class

Every class declared in Semantifyr implicitly extends Anything from the standard library. Anything provides empty init and tran transitions:

class Anything {
  tran { }
  init { }
}

A class has one init, one implicit tran (named main) and one anonymous prop, so declaring your own overrides the inherited one, with or without redefine; a second one of a kind in the same class is a duplicate name (OXSTS.DUPLICATE_NAME). See Redefining members.

Class Declaration

A class declaration consists of the class keyword, a name, an optional superclass, and a body in { }. Members may appear in any order.

class Counter {
  var value: int := 0

  tran increment() {
    value := value + 1
  }

  prop isPositive(): bool {
    return value > 0
  }
}

A class with no members may be written with an empty body.

class Sentinel {
}

Or without any.

class Sentinel

tip

Generally Semantifyr is lenient with the use or absence of semicolons ;.

Abstract Classes

abstract class cannot be instantiated directly, so it cannot be a @VerificationCase (OXSTS.ABSTRACT_VERIFICATION_CASE). An abstract class may declare abstract members (without bodies) that concrete subclasses must redefine. A concrete @VerificationCase declares or inherits the anonymous prop it checks (OXSTS.MISSING_PROPERTY).

abstract class Shape {
  abstract prop area(): int
}

Inheritance

A class extends one superclass, listed after :.

abstract class Shape {
  abstract prop area(): int
}

class Square : Shape {
  var side: int := 1

  redefine prop area(): int {
    return side * side
  }
}

caution

The grammar accepts several superclasses separated by commas, but a class has one superclass: the validator rejects every superclass after the first (OXSTS.MULTIPLE_INHERITANCE).

Redefining Members

redefine overrides an inherited member of the same name. A redefined transition or property takes as many parameters as the inherited one (OXSTS.REDEFINITION_SIGNATURE_MISMATCH), and a redefined property's return type or feature's type must be assignable to the inherited one (OXSTS.TYPE_MISMATCH); parameter types may differ. Variables cannot be redefined. Two members of one class that redefine the same inherited member are rejected (OXSTS.DUPLICATE_REDEFINITION). Redefining is the primary mechanism by which semantic libraries specialize behavior.

redefine tran fire() {
  inline target.activate()
}

redefine prop evaluate(): int {
  return value
}

redefine contains entryAction: SendAction

self

Inside a class body, self refers to the current instance of that class or feature. It is typically used to pass the current instance as an argument, or to reach a member whose name a parameter or a local variable reuses. Outside a class, in a global feature or a record, self is rejected (OXSTS.SELF_OUTSIDE_CLASS).

class Counter {
  contains parent: Group

  redefine init {
    inline parent.register(self)
  }
}