Packages

o

edu.cmu.cs.ls.keymaerax.btactics

DebuggingTactics

object DebuggingTactics

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. DebuggingTactics
  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 assert(cond: (Sequent, Position) ⇒ Boolean, message: ⇒ String): BuiltInPositionTactic

    assert is a no-op tactic that raises a tactic assertion error if the provable does not satisfy a condition at position pos.

  6. def assert(cond: (Sequent, Position) ⇒ Boolean, message: ⇒ String, ex: (String) ⇒ Throwable): BuiltInPositionTactic

    assert is a no-op tactic that raises an error if the provable does not satisfy a condition at position pos.

  7. def assert(cond: (Sequent) ⇒ Boolean, message: ⇒ String): BuiltInTactic

    assert is a no-op tactic that raises a tactic assertion error if the provable does not satisfy a condition on the sole subgoal.

  8. def assert(cond: (Sequent) ⇒ Boolean, message: ⇒ String, ex: (String) ⇒ Throwable): BuiltInTactic

    assert is a no-op tactic that raises an error if the provable does not satisfy a condition on the sole subgoal.

  9. def assert(fml: Formula, message: ⇒ String): DependentPositionWithAppliedInputTactic

    assert is a no-op tactic that raises a tactic assertion error if the provable has not the expected formula at the specified position.

  10. def assert(fml: Formula, message: ⇒ String, ex: (String) ⇒ Throwable): DependentPositionWithAppliedInputTactic

    assert is a no-op tactic that raises an error if the provable has not the expected formula at the specified position.

  11. def assert(anteSize: Int, succSize: Int, msg: ⇒ String = ""): BuiltInTactic

    assert is a no-op tactic that raises a tactic assertion error if the provable is not of the expected size.

  12. def assert(anteSize: Int, succSize: Int, msg: ⇒ String, ex: (String) ⇒ Throwable): BuiltInTactic

    assert is a no-op tactic that raises an error if the provable is not of the expected size.

  13. def assertAt(msg: ⇒ String, assertion: (Expression) ⇒ Boolean, ex: (String) ⇒ Throwable): BuiltInPositionTactic
  14. def assertAt(msg: (Expression) ⇒ String, assertion: (Expression) ⇒ Boolean, ex: (String) ⇒ Throwable = new TacticAssertionError(_)): BuiltInPositionTactic

    Assert that the assertion holds at a the specified position.

    Assert that the assertion holds at a the specified position. Could be a non-top-level position. Analogous to debugAt.

    msg

    The message to display.

    assertion

    The assertion.

  15. def assertE(expected: ⇒ Expression, message: ⇒ String): DependentPositionWithAppliedInputTactic

    assertE is a no-op tactic that raises a tactic assertion error if the provable has not the expected expression at the specified position.

  16. def assertE(expected: ⇒ Expression, message: ⇒ String, ex: (String) ⇒ Throwable): DependentPositionWithAppliedInputTactic

    assertE is a no-op tactic that raises an error if the provable has not the expected expression at the specified position.

  17. def assertOnAll(cond: (Sequent) ⇒ Boolean, message: ⇒ String, ex: (String) ⇒ Throwable = new TacticAssertionError(_)): BuiltInTactic

    assertOnAll is a no-op tactic that raises an error the provable does not satisfy a condition on all subgoals.

  18. def assertProvableSize(provableSize: Int, ex: (String) ⇒ Throwable = new TacticAssertionError(_)): BuiltInTactic

    asserts that the provable has provableSize many subgoals.

  19. def assertX(expected: Expression, msg: String): DependentPositionWithAppliedInputTactic
    Annotations
    @Tactic( ("Assert", "assert") , "assert" , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
  20. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  21. def debug(message: ⇒ String, doPrint: Boolean = DEBUG, printer: (ProvableSig) ⇒ String = _.toString): BuiltInTactic

    debug is a no-op tactic that prints a message and the current provable, if doPrint (defaults to the system property DEBUG) is true.

  22. def debugAt(message: ⇒ String, doPrint: Boolean = DEBUG): BuiltInPositionTactic

    debug is a no-op tactic that prints a message and the current provable, if the system property DEBUG is true.

  23. def debugX(msg: String): StringInputTactic
    Annotations
    @Tactic( ("Debug", "debug") , "debug" , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
  24. def done(msg: Option[String], lemmaName: Option[String]): StringInputTactic
    Annotations
    @Tactic( ("Done","done") , "done" , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
  25. def done(msg: String, storeLemma: Option[String]): StringInputTactic
  26. def done(msg: String): StringInputTactic
  27. lazy val done: BelleExpr

  28. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  29. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  30. def error(s: ⇒ String, e: (String) ⇒ BelleThrowable = new TacticInapplicableFailure(_)): BuiltInTactic

    Indicates a failed attempt that triggers proof search.

  31. def error(e: Throwable): BuiltInTactic
  32. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  33. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  34. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  35. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  36. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  37. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  38. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  39. def pending(tactic: String): StringInputTactic

    Placeholder for a tactic string that is not executed.

    Placeholder for a tactic string that is not executed.

    Annotations
    @Tactic( "pending" , "pending" , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
  40. def pendingX(tactic: String): StringInputTactic
    Annotations
    @Tactic( "pendingX" , "pendingX" , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
  41. def print(message: ⇒ String): BuiltInTactic

    print is a no-op tactic that prints a message and the current provable, regardless of DEBUG being true or false

  42. def printIndexed(message: ⇒ String): BuiltInTactic

    printIndexed is a no-op tactic that prints a message and the current provable (verbose sequent with formula indices), regardless of DEBUG being true or false

  43. def printX(msg: String): StringInputTactic
    Annotations
    @Tactic( ("Print", "print") , "print" , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
  44. def recordQECall(): BuiltInTactic
  45. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  46. def toString(): String
    Definition Classes
    AnyRef → Any
  47. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  48. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  49. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped