Packages

case class VariableSets(boundVars: Set[Variable], mustBoundVars: Set[Variable], freeVars: Set[Variable], tabooVars: Set[Variable], tabooFunctions: Set[Ident], tabooFacts: Set[Ident]) extends Product with Serializable

Stores results of variable set computations for Kaisar proofs

boundVars

All program variables which are bound at some point in the proof, except Phi assignments

mustBoundVars

All program variables which are bound on every path in proof.

freeVars

All program variables which appear free in proof without surrounding must-binder

tabooVars

All program variables which are taboo (not allowed to be referenced), usually because they are ghosts

tabooFunctions

All function symbols which are taboo to reference, usually because they are inverse ghosts

tabooFacts

All fact variables which are taboo to reference, usually because they are inverse ghosts

Linear Supertypes
Serializable, Serializable, Product, Equals, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. VariableSets
  2. Serializable
  3. Serializable
  4. Product
  5. Equals
  6. AnyRef
  7. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new VariableSets(boundVars: Set[Variable], mustBoundVars: Set[Variable], freeVars: Set[Variable], tabooVars: Set[Variable], tabooFunctions: Set[Ident], tabooFacts: Set[Ident])

    boundVars

    All program variables which are bound at some point in the proof, except Phi assignments

    mustBoundVars

    All program variables which are bound on every path in proof.

    freeVars

    All program variables which appear free in proof without surrounding must-binder

    tabooVars

    All program variables which are taboo (not allowed to be referenced), usually because they are ghosts

    tabooFunctions

    All function symbols which are taboo to reference, usually because they are inverse ghosts

    tabooFacts

    All fact variables which are taboo to reference, usually because they are inverse ghosts

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. def ++(other: VariableSets): VariableSets

    Set union

  4. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  5. def addBoundVars(v: Set[Variable]): VariableSets
  6. def addFreeVars(v: Set[Variable]): VariableSets
  7. def addTabooFacts(p: Set[Ident]): VariableSets
  8. def addTabooFuncs(f: Set[Ident]): VariableSets
  9. def addTabooVars(v: Set[Variable]): VariableSets
  10. def allVars: Set[Variable]
  11. def andThen(other: VariableSets): VariableSets

    Combine sequential steps.

    Combine sequential steps. Allows tighter free-variables computation

  12. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  13. val boundVars: Set[Variable]
  14. def choice(other: VariableSets): VariableSets

    Combine alternative branches.

    Combine alternative branches. Like ++ but must-bound is intersected

  15. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  16. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  17. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  18. def forgetBound: VariableSets
  19. val freeVars: Set[Variable]
  20. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  21. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  22. val mustBoundVars: Set[Variable]
  23. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  24. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  25. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  26. def option: VariableSets

    Clear must-bound variables for optional statements

  27. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  28. val tabooFacts: Set[Ident]
  29. val tabooFunctions: Set[Ident]
  30. val tabooVars: Set[Variable]
  31. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  32. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  33. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from Serializable

Inherited from Serializable

Inherited from Product

Inherited from Equals

Inherited from AnyRef

Inherited from Any

Ungrouped