Packages

o

edu.cmu.cs.ls.keymaerax.infrastruct

StaticSemanticsTools

object StaticSemanticsTools

Additional tools read off from the static semantics for the tactics.

See also

edu.cmu.cs.ls.keymaerax.core.StaticSemantics

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. StaticSemanticsTools
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  5. def bindingVars(program: Program): SetLattice[Variable]

    The set of variables that the top-level operator of this program is binding itself, so not those variables that are only bound because of operators in subprograms.

  6. def bindingVars(formula: Formula): SetLattice[Variable]

    The set of variables that the top-level operator of this formula is binding itself, so not those variables that are only bound because of operators in subformulas.

  7. def boundAt(program: Program, pos: PosInExpr): SetLattice[Variable]

    The set of variables that, if they occurred at program(pos) would be bound occurrences, because there was an operator in program on the path to pos for which it was binding.

    The set of variables that, if they occurred at program(pos) would be bound occurrences, because there was an operator in program on the path to pos for which it was binding. If an occurrence of a variable at program(pos) is not boundAt(program,pos) then it is a free occurrence.

    See also

    Context.at()

  8. def boundAt(formula: Formula, pos: PosInExpr): SetLattice[Variable]

    The set of variables that, if they occurred at formula(pos) would be bound occurrences, because there was an operator in formula on the path to pos for which it was binding.

    The set of variables that, if they occurred at formula(pos) would be bound occurrences, because there was an operator in formula on the path to pos for which it was binding. If an occurrence of a variable at formula(pos) is not boundAt(formula,pos) then it is a free occurrence.

    See also

    Context.at()

  9. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  10. def dependencies(ode: DifferentialProgram): Map[Variable, Set[Variable]]
  11. def dependencies(program: Program): Map[Variable, Set[Variable]]

    Compute all variable dependencies, i.e.

    Compute all variable dependencies, i.e. the set of all variables that each variable depends on by data flow dependencies.

    Example: 

    1. dependencies("a:=-b;{x'=v,v'=a,t'=1}".asProgram) == (a->{b}, x->{v}, v->{a}, t->{})
dependencies("a:=-b+a;{x'=y,y'=-x,z'=x^2+y}".asProgram) == (a->{a,b}, x->{y}, y->{x}, z->{x,y})
    To do

    could respect control-flow dependencies too but might degenerate.

    Note

    so far only a simple data flow dependencies ignoring all control flow.

    ,

    currently ignores some differential symbol dependencies.

    ,

    ignores self-dependency from x'=1

  12. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  13. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  14. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  15. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  16. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  17. def inverseDependencies(deps: Map[Variable, List[Variable]]): Map[Variable, List[Variable]]

    Inverse of the dependency relation deps

  18. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  19. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  20. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  21. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  22. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  23. def toString(): String
    Definition Classes
    AnyRef → Any
  24. def transitiveDependencies(ode: DifferentialProgram): Map[Variable, List[Variable]]
  25. def transitiveDependencies(program: Program): Map[Variable, List[Variable]]

    Compute all transitive variable dependencies, i.e.

    Compute all transitive variable dependencies, i.e. the set of all variables that each variable depends on directly or indirectly by data flow dependencies. The order of the dependent variables will be by approximate topological sort, so variables after the ones they depend on themselves.

    Example: 

    1. dependencies("{x'=v,v'=a,a'=j,t'=1}".asProgram) == (x->{j,a,v}, v->{j,a}, a->{j}, t->{})
dependencies("a:=-b;{x'=v,v'=a,t'=1}".asProgram) == (a->{b}, x->{a,v}, v->{a}, t->{})
dependencies("a:=-b+a;{x'=y,y'=-x,z'=x^2+y}".asProgram) == (a->{a,b}, x->{x,y}, y->{y,x}, z->{x,y})
    To do

    could respect control-flow dependencies too but might degenerate.

    Note

    so far only a simple data flow dependencies ignoring all control flow.

    ,

    currently ignores some differential symbol dependencies.

    ,

    ignores self-dependency from x'=1

  26. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  27. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  28. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped