Packages

abstract class Semantics[Exp, Abs, Addr, Time] extends AnyRef

This is where the interface of a language's semantics is defined. By defining the semantics of a language, you get an abstract abstract machine for free (but you might need to adapt existing lattices to support values from your language).

Semantics should be defined as small-step operational semantics. To define a semantics, you have to implement the Semantics trait. You'll need to specialize it on the type of expression of your language (e.g., ??? for ANF, ANFSemantics specializes on ANFExp). To do so, you need to define what actions should be taken when:

  1. Evaluating an expression e (stepEval) 2. Continuing evaluation when a value v has been reached (stepKont)

To have a simple overview of how semantics should be defined, look at the ANFSemantics.scala, as it defines semantics of ANF Scheme, a very lightweight language. A more complex definition resides in SchemeSemantics.scala.

Linear Supertypes
AnyRef, Any
Known Subclasses
BaseSchemeSemantics, SchemeSemantics
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Semantics
  2. AnyRef
  3. Any
Implicitly
  1. by any2stringadd
  2. by StringFormat
  3. by Ensuring
  4. by ArrowAssoc
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new Semantics()(implicit arg0: Expression[Exp], arg1: JoinLattice[Abs], arg2: Address[Addr], arg3: Timestamp[Time])

Abstract Value Members

  1. abstract def parse(program: String): Exp

    Defines how to parse a program

  2. abstract def stepEval(e: Exp, env: Environment[Addr], store: Store[Addr, Abs], t: Time): Set[Action[Exp, Abs, Addr]]

    Defines what actions should be taken when an expression e needs to be evaluated, in environment env with store store

  3. abstract def stepKont(v: Abs, frame: Frame, store: Store[Addr, Abs], t: Time): Set[Action[Exp, Abs, Addr]]

    Defines what actions should be taken when a value v has been reached, and the topmost frame is frame

Concrete Value Members

  1. implicit def actionToSet(action: Action[Exp, Abs, Addr]): Set[Action[Exp, Abs, Addr]]
  2. def initialBindings: Iterable[(String, Addr, Abs)]

    Defines the elements in the initial environment/store

  3. def initialEnv: Iterable[(String, Addr)]
  4. def initialStore: Iterable[(Addr, Abs)]
  5. implicit def mfActionToActions(mf: MayFail[Action[Exp, Abs, Addr]]): Set[Action[Exp, Abs, Addr]]
  6. implicit def mfToActions(mf: MayFail[Set[Action[Exp, Abs, Addr]]]): Set[Action[Exp, Abs, Addr]]
  7. def stepReceive(self: Any, mname: String, margsv: List[Abs], d: Exp, env: Environment[Addr], store: Store[Addr, Abs], t: Time): Set[Action[Exp, Abs, Addr]]

    WIP

  8. object Action extends ActionHelpers[Exp, Abs, Addr]