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, tran, and havoc transitions:

class Anything {
  tran { }
  init { }
  havoc { }
}

Because these transitions are inherited, declaring your own init, implicit tran (named main), or havoc requires redefine. See Redefining members.

Class Declaration

A class declaration consists of the class keyword, a name, an optional list of superclasses, 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. An abstract class may declare abstract members (without bodies) that concrete subclasses must redefine.

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

Inheritance

A class extends one or more superclasses listed after :, separated by commas.

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

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

Redefining Members

redefine overrides an inherited member of the same name. The redefining member must match the signature (parameter types and return type for transitions and properties). 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.

class Counter {
  contains parent: Group

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