Packages

  • package root
    Definition Classes
    root
  • class AAM[Exp, Abs, Addr, Time] extends EvalKontMachine[Exp, Abs, Addr, Time]

    Implementation of a CESK machine following the AAM approach (Van Horn, David, and Matthew Might.

    Implementation of a CESK machine following the AAM approach (Van Horn, David, and Matthew Might. "Abstracting abstract machines." ACM Sigplan Notices. Vol. 45. No. 9. ACM, 2010).

    A difference with the paper is that we separate the continuation store (KontStore) from the value store (Store). That simplifies the implementation of both stores, and the only change it induces is that we are not able to support first-class continuation as easily (we don't support them at all, but they could be added).

    Also, in the paper, a CESK state is made of 4 components: Control, Environment, Store, and Kontinuation. Here, we include the environment in the control component, and we distinguish "eval" states from "continuation" states. An eval state has an attached environment, as an expression needs to be evaluated within this environment, whereas a continuation state only contains the value reached.

    Definition Classes
    root
  • AAMOutput
  • Control
  • ControlError
  • ControlEval
  • ControlKont
  • HaltKontAddress
  • KontAddr
  • NormalKontAddress
  • Output
  • State

case class State(control: AAM.Control, store: Store[Addr, Abs], kstore: KontStore[KontAddr], a: KontAddr, t: Time) extends Product with Serializable

A machine state is made of a control component, a value store, a continuation store, and an address representing where the current continuation lives.

Linear Supertypes
Serializable, Serializable, Product, Equals, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. State
  2. Serializable
  3. Serializable
  4. Product
  5. Equals
  6. AnyRef
  7. 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 State(control: AAM.Control, store: Store[Addr, Abs], kstore: KontStore[KontAddr], a: KontAddr, t: Time)

Value Members

  1. val a: KontAddr
  2. val control: AAM.Control
  3. def halted: Boolean

    Checks if the current state is a final state.

    Checks if the current state is a final state. It is the case if it reached the end of the computation, or an error

  4. val kstore: KontStore[KontAddr]
  5. def step(sem: Semantics[Exp, Abs, Addr, Time]): Set[State]

    Computes the set of states that follow the current state

  6. def stepAnalysis[L](analysis: Analysis[L, Exp, Abs, Addr, Time], current: L): L
  7. val store: Store[Addr, Abs]
  8. def subsumes(that: State): Boolean

    Checks whether a states subsumes another, i.e., if it is "bigger".

    Checks whether a states subsumes another, i.e., if it is "bigger". This is used to perform subsumption checking when exploring the state space, in order to avoid exploring states for which another state that subsumes them has already been explored.

  9. val t: Time
  10. def toString(): String
    Definition Classes
    State → AnyRef → Any