Packages

o

edu.cmu.cs.ls.keymaerax.core

StaticSemantics

object StaticSemantics

The static semantics of differential dynamic logic. This object defines the static semantics of differential dynamic logic in terms of the free variables and bound variables that expressions have as well as their signatures.

Example: 

  1. val fml = Imply(Greater(Variable("x",None,Real), Number(5)),
  Forall(Seq(Variable("y",None,Real)),
    GreaterEqual(Variable("x",None,Real), FuncOf(Function("f",None,Real,Real), Variable("y",None,Real)))))
// determine the static semantics of the above formula
val stat = StaticSemantics(fml)
println("Free variables  " + stat.fv)
println("Bound variables " + stat.bv)
// determine all function, predicate and program constants occurring in the above formula
println("Signature       " + StaticSemantics.signature(fml))
// determine all symbols occurring in the above formula
println("Symbols         " + StaticSemantics.symbols(fml))
Note

soundness-critical

See also

Section 2.3 in Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017.

Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981

edu.cmu.cs.ls.keymaerax.infrastruct.StaticSemanticsTools

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

Type Members

  1. sealed case class VCF(fv: SetLattice[Variable], bv: SetLattice[Variable]) extends Product with Serializable

    Variable Categories for Formulas: Structure recording which names are free or bound in a formula.

    Variable Categories for Formulas: Structure recording which names are free or bound in a formula.

    fv

    Free names (maybe read)

    bv

    Bound names (maybe written)

    Note

    The core does not uses bv.

  2. sealed case class VCP(fv: SetLattice[Variable], bv: SetLattice[Variable], mbv: SetLattice[Variable]) extends Product with Serializable

    Variable Categories for Programs: Structure recording which names are free, bound, or must-bound in a program.

    Variable Categories for Programs: Structure recording which names are free, bound, or must-bound in a program.

    fv

    Free names (maybe read)

    bv

    Bound names (maybe written on some paths)

    mbv

    Must-bound names (definitely written on all paths).

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. def apply(a: Program): VCP

    Compute the static semantics of program a, i.e., its set of free and bound and must-bound variables.

  5. def apply(f: Formula): VCF

    Compute the static semantics of formula f, i.e., its set of free and bound variables.

  6. def apply(t: Term): SetLattice[Variable]

    Compute the static semantics of term t, i.e., the set of its free variables.

  7. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  8. def boundVars(s: Sequent): SetLattice[Variable]

    The set BV(a) of bound variables of a sequent.

  9. def boundVars(a: Program): SetLattice[Variable]

    The set BV(a) of bound variables of program a.

  10. def boundVars(f: Formula): SetLattice[Variable]

    The set BV(f) of bound variables of formula f.

  11. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  12. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  13. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  14. def finalize(): scala.Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  15. def freeVars(s: Sequent): SetLattice[Variable]

    The set FV(a) of free variables of a sequent.

  16. def freeVars(e: Expression): SetLattice[Variable]

    The set FV(e) of free variables of expression e.

  17. def freeVars(a: Program): SetLattice[Variable]

    The set FV(a) of free variables of program a.

  18. def freeVars(f: Formula): SetLattice[Variable]

    The set FV(f) of free variables of formula f.

  19. def freeVars(term: Term): SetLattice[Variable]

    The set FV(term) of free variables of term.

  20. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  21. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  22. def isDifferential(e: Expression): Boolean

    Check whether expression e is literally a properly differential term/expression, i.e.

    Check whether expression e is literally a properly differential term/expression, i.e. mentions differentials or differential symbols free.

    Note

    Only verbatim mentions are counted, so not via indirect Space dependency.

    ,

    (5)' and (c())' will be considered as non-differential terms on account of not mentioning variables, but (x+y)' is differential.

    ,

    AtomicODE uses isDifferential to ensure explicit differential equation x'=e has no primes in e.

    ,

    ODESystem uses isDifferential to ensure explicit differential equation x'=e&Q has no primes in Q.

    ,

    For proper terms (not using Anything), freeVars is finite so .symbols==.toSet, so checks for literally free DifferentialSymbols.

  23. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  24. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  25. final def notify(): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  26. final def notifyAll(): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  27. def signature(s: Sequent): Set[NamedSymbol]

    The signature of a sequent.

  28. def signature(program: Program): Set[NamedSymbol]

    The signature of a program, i.e., set of function, predicate, and atomic program symbols occurring in it.

    The signature of a program, i.e., set of function, predicate, and atomic program symbols occurring in it.

    Note

    Soundness-critical in data structure invariant for interpreted functions.

    ,

    Not soundness-critical otherwise since substitution only uses it in old USubstChurch not in new USubstOne.

  29. def signature(formula: Formula): Set[NamedSymbol]

    The signature of a formula, i.e., set of (non-logical) function, predicate, predicational, and atomic program symbols occurring in it.

    The signature of a formula, i.e., set of (non-logical) function, predicate, predicational, and atomic program symbols occurring in it.

    Note

    Soundness-critical in data structure invariant for interpreted functions.

    ,

    Not soundness-critical otherwise since substitution only uses it in old USubstChurch not in new USubstOne.

  30. def signature(term: Term): Set[NamedSymbol]

    The signature of a term, i.e., set of (non-logical) function/functional symbols occurring in it.

    The signature of a term, i.e., set of (non-logical) function/functional symbols occurring in it. Disregarding number literals.

    Note

    Soundness-critical in data structure invariant for interpreted functions.

    ,

    Not soundness-critical otherwise since substitution only uses it in old USubstChurch not in new USubstOne.

  31. def signature(e: Expression): Set[NamedSymbol]

    The signature of expression e.

    The signature of expression e.

    Example: 

    1. signature(e).toList.sort            // sorts by compare of NamedSymbol, by name and index
signature(e).toList.sortBy(_.name)  // sorts alphabetically by name, ignores indices
    Note

    Result will not be order stable, so order could be different on different runs of the prover.

    ,

    Soundness-critical in data structure invariant for interpreted functions.

    ,

    Not soundness-critical otherwise since substitution only uses it in old USubstChurch not in new USubstOne.

  32. def spaceVars(space: Space): SetLattice[Variable]

    The variables and differential symbols that are in the given state space.

    The variables and differential symbols that are in the given state space.

    space

    The state space whose set (lattice) of variables and differential variables to compute.

    • AnyArg returns the SetLattice.allVars.
    • Except(taboo) returns all variables except spaceTaboos(taboos), i.e. all variables and differential variables except the taboo x and x'.
  33. def symbols(s: Sequent): Set[NamedSymbol]

    Any symbol occurring verbatim in a sequent, whether free or bound variable or function or predicate or program constant

  34. def symbols(p: Program): Set[NamedSymbol]

    Any (non-logical) symbol occurring verbatim in program, whether free or bound variable or function or predicate or program constant.

  35. def symbols(f: Formula): Set[NamedSymbol]

    Any (non-logical) symbol occurring verbatim in formula, whether free or bound variable or function or predicate or program constant.

  36. def symbols(t: Term): Set[NamedSymbol]

    Any (non-logical) symbol occurring verbatim in term, whether variable or function.

  37. def symbols(e: Expression): Set[NamedSymbol]

    Any (non-logical) symbols occurring verbatim in expression e, whether free or bound variable or function or predicate or program constant.

  38. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  39. def toString(): String
    Definition Classes
    AnyRef → Any
  40. def vars(e: Expression): SetLattice[Variable]

    The set var(e) of variables of expression e, whether free or bound.

  41. final def wait(): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  42. final def wait(arg0: Long, arg1: Int): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  43. final def wait(arg0: Long): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped