Type Members

1.  case class AForLoop(idx: Ident, idx0: Term, conv: Formula, body: AngelStrategy, idxUp: Term, guardDelta: Option[Term]) extends AngelStrategy with Product with Serializable
2.  case class ALoop(conv: Formula, body: AngelStrategy) extends AngelStrategy with Product with Serializable

   Angelic while loop with decidable convergence/guard formula

3.  case class AODE(ode: ODESystem, dur: Term) extends AngelStrategy with Product with Serializable

   Differential equation with (concrete) angelic duration.

4.  sealed trait ASTNode extends AnyRef
5.  case class ASwitch(branches: List[(Formula, AngelStrategy)]) extends AngelStrategy with Product with Serializable

   Angelic switch statement with decidable branch guards

6.  sealed trait AngelStrategy extends AnyRef

   Directly executable, simply-typed strategy for Angel player

7.  sealed trait AsgnPat extends ASTNode
8.  case class Assert(pat: IdentPat, f: Formula, m: Method) extends Statement with Product with Serializable
9.  case class Assume(pat: IdentPat, f: Formula) extends Statement with Product with Serializable
10.  case class AtomicODEStatement(dp: AtomicODE, solFact: IdentPat = Nothing) extends DiffStatement with Product with Serializable
11.  case class Auto() extends Method with Product with Serializable
12.  trait BasicDemonStrategy[number <: Numeric[number, Ternary]] extends AnyRef

    Wrappable interface for Demon strategies.

    Wrappable interface for Demon strategies. While this interface is not "simpler" than DemonStrategy, it is designed to work seamlessly with the output of SimpleStrategy.apply. i.e., if you wish to write a raw DemonStrategy, you will have to be familiar with the SimpleStrategy.apply implementation, but not if you write BasicDemonStrategy. Also simplifies initial-state computation.

    See also

    DemonStrategy

    WrappedDemonStrategy

13.  case class Block(ss: Statements) extends Statement with Product with Serializable
14.  case class BoxChoice(left: Statement, right: Statement) extends Statement with Product with Serializable
15.  case class BoxChoiceProgress(bc: BoxChoice, onBranch: Int, progress: Statement) extends MetaNode with Product with Serializable
16.  case class BoxLoop(s: Statement, ih: Option[(IdentPat, Formula, Option[Formula])] = None) extends Statement with Product with Serializable
17.  case class BoxLoopProgress(boxLoop: BoxLoop, progress: Statement) extends MetaNode with Product with Serializable
18.  case class ByProof(proof: Statements) extends Method with Product with Serializable
19.  case class Comment(str: String) extends MetaNode with Product with Serializable

    Note this is not for comments parsed from source files since the parser strips out comments.

    Note this is not for comments parsed from source files since the parser strips out comments. This is used for the insertion of machine-generated comments in machine-generated Kaisar files

20.  case class ConclusionDecl(thmName: Ident) extends KaisarDecl with Product with Serializable

    Display the already-proved conclusion of a proof

21.  case class Context(s: Statement) extends Product with Serializable
22.  sealed trait ContextQuery extends AnyRef
23.  sealed trait ContextResult extends AnyRef
24.  case class DebugArith(opt: Boolean) extends OptionSpec with Product with Serializable

    When arith debug, every formula checked in a proof search is printed

25.  case class Decls(dcls: List[KaisarDecl]) extends KaisarDecl with Product with Serializable

    List of declarations evaluated sequentially

26.  class DemonException extends Exception
27.  trait DemonStrategy[T] extends AnyRef

    Interface for drivers implementing Demon strategies / implementing an environment or hardware/simulation platform

    Interface for drivers implementing Demon strategies / implementing an environment or hardware/simulation platform

    See also

    BasicDemonStrategy

28.  case class DeterritorializePass(tt: TimeTable) extends Product with Serializable
29.  final case class DiffCollection(atoms: Set[AtomicODEStatement], ghosts: Set[AtomicODEStatement], inverseGhosts: Set[AtomicODEStatement]) extends Product with Serializable
30.  case class DiffGhostStatement(ds: DiffStatement) extends DiffStatement with Product with Serializable
31.  case class DiffInduction() extends Method with Product with Serializable
32.  case class DiffProductStatement(l: DiffStatement, r: DiffStatement) extends DiffStatement with Product with Serializable
33.  sealed trait DiffStatement extends ASTNode
34.  case class DomAnd(l: DomainStatement, r: DomainStatement) extends DomainStatement with Product with Serializable
35.  case class DomAssert(x: IdentPat, f: Formula, child: Method) extends DomainFact with Product with Serializable
36.  case class DomAssume(x: IdentPat, f: Formula) extends DomainFact with Product with Serializable
37.  final case class DomCollection(assumptions: Set[DomAssume], assertions: List[DomAssert], weakens: Set[DomainStatement], modifiers: Set[DomModify]) extends Product with Serializable

    Note: assertions are a list because it matters what order assertions are proved in.

    Note: assertions are a list because it matters what order assertions are proved in. Order does not matter for the others.

38.  case class DomModify(id: IdentPat, x: Variable, f: Term) extends DomainStatement with Product with Serializable
39.  case class DomWeak(dc: DomainStatement) extends DomainStatement with Product with Serializable
40.  sealed trait DomainFact extends DomainStatement
41.  sealed trait DomainStatement extends ASTNode
42.  class ElaborationPass extends AnyRef
43.  class Environment[number <: Numeric[number, Ternary]] extends AnyRef

    Runtime state of executed strategy

44.  case class Exhaustive() extends Method with Product with Serializable
45.  case class For(metX: Ident, met0: Term, metIncr: Term, conv: Option[Assert], guard: Assume, body: Statement, guardDelta: Option[Term] = None) extends Statement with Product with Serializable
46.  case class ForProgress(forth: For, progress: Statement) extends MetaNode with Product with Serializable
47.  case class ForwardSelector(forward: ProofTerm) extends Selector with Product with Serializable
48.  case class Ghost(s: Statement) extends Statement with Product with Serializable
49.  case class GuardDone(delta: Option[Term]) extends Method with Product with Serializable
50.  case class Hypothesis() extends Method with Product with Serializable
51.  case class InverseDiffGhostStatement(ds: DiffStatement) extends DiffStatement with Product with Serializable
52.  case class InverseGhost(s: Statement) extends Statement with Product with Serializable
53.  sealed trait KaisarDecl extends AnyRef
54.  class KaisarKeywordParser extends AnyRef
55.  case class KnownFalse() extends Ternary with Product with Serializable
56.  case class KnownTrue() extends Ternary with Product with Serializable
57.  case class Label(st: LabelDef, snapshot: Option[Snapshot] = None) extends Statement with Product with Serializable
58.  case class LetDecl(ls: LetSym) extends KaisarDecl with Product with Serializable

    Define a function, predicate, or program which can be reused across proofs

59.  case class LetSym(f: Ident, args: List[Ident], e: Expression) extends Statement with Product with Serializable
60.  case class LiteralMetric(delta: Number, bound: Number) extends Metric with Product with Serializable
61.  case class Match(pat: Term, e: Expression) extends Statement with Product with Serializable
62.  sealed trait MetaNode extends Statement
63.  sealed trait Method extends ASTNode
64.  sealed trait Metric extends AnyRef
65.  case class Modify(ids: List[Ident], mods: List[(Variable, Option[Term])]) extends Statement with Product with Serializable
66.  case class NoPat() extends AsgnPat with Product with Serializable
67.  case class NoValueException(nodeID: Int = -1, msg: String) extends Exception with Product with Serializable

    Indicates that we tried to evaluate something whose value could not be determined

68.  case class Note(x: Ident, proof: ProofTerm, annotation: Option[Formula] = None) extends Statement with Product with Serializable
69.  trait NumberFactory[Truth, N <: Numeric[N, Truth]] extends AnyRef
70.  trait Numeric[T, Truth] extends AnyRef

    Trait for different arithmetic representations supported for system execution

71.  case class OptionPragma(optionSpec: OptionSpec) extends PragmaSpec with Product with Serializable

    The option pragma is used to configure settings

72.  sealed trait OptionSpec extends AnyRef

    Language of option specifications

73.  case class PatternSelector(e: Term) extends Selector with Product with Serializable
74.  case class Phi(asgns: Statement) extends MetaNode with Product with Serializable
75.  class Play[N <: Numeric[N, Ternary]] extends AnyRef

    Interpreter for strategies

76.  case class Pragma(ps: PragmaSpec) extends MetaNode with Product with Serializable

    Used for features which are not fundamentally part of the language, but more convenience features of the implementation.

    Used for features which are not fundamentally part of the language, but more convenience features of the implementation. Used for setting options including those useful for debugging or profiling

77.  case class PragmaDecl(ls: PragmaSpec) extends KaisarDecl with Product with Serializable

    Apply a pragma directive to the entire remainder of the file

78.  sealed trait PragmaSpec extends AnyRef

    Language of pragma statements

79.  case class PrintExpr(e: Expression) extends Printable with Product with Serializable
80.  case class PrintGoal(printable: Printable) extends MetaNode with Product with Serializable
81.  case class PrintString(msg: String) extends Printable with Product with Serializable
82.  sealed trait Printable extends AnyRef
83.  case class ProgramAssignments(x: Variable, onlySSA: Boolean = false) extends ProofTerm with Product with Serializable
84.  case class ProgramVar(x: Variable) extends ProofTerm with Product with Serializable
85.  case class ProofApp(m: ProofTerm, n: ProofTerm) extends ProofTerm with Product with Serializable
86.  case class ProofInstance(e: Expression) extends ProofTerm with Product with Serializable
87.  sealed trait ProofTerm extends ASTNode
88.  case class ProofVar(x: Ident) extends ProofTerm with Product with Serializable
89.  case class Prop() extends Method with Product with Serializable
90.  case class ProvablyConstantMetric(delta: Term, bound: Term, isIncreasing: Boolean, taboos: Set[Variable]) extends Metric with Product with Serializable
91.  case class ProveODE(ds: DiffStatement, dc: DomainStatement) extends Statement with Product with Serializable
92.  case class ProvesDecl(thmName: Ident, conclusion: Formula) extends KaisarDecl with Product with Serializable

    Check whether given conclusion follows from given proof

93.  case class QAssignments(x: Variable, onlySSA: Boolean) extends ContextQuery with Product with Serializable

    Matches all assignments which assign a given variable x.

    Matches all assignments which assign a given variable x. The subscript of x is ignored so that a simple search for x will capture its SSA-variants such as x_1.

94.  case class QElaborate(cq: ContextQuery) extends ContextQuery with Product with Serializable

    QElaborate instructs the context to execute query cq normally, then fully elaborate all (user-defined and internal) function symbols appearing in the result.

95.  case class QNil() extends ContextQuery with Product with Serializable

    Matches nothing.

    Matches nothing. Algebraic unit of query language.

96.  case class QPhi(phi: Phi, cq: ContextQuery) extends ContextQuery with Product with Serializable

    Applies a query cq under an assignment.

    Applies a query cq under an assignment. Assuming queries are applied to (light) SSA-form contexts, the QPhi is only needed for (inlined) Phi assignments, as they are the only assignments which ever shadow another.

97.  case class QProgramVar(x: Variable) extends ContextQuery with Product with Serializable

    Matches all facts which mention a given program variable

98.  case class QProofTerm(pt: ProofTerm) extends ContextQuery with Product with Serializable

    Query corresponding to a proof term selector.

    Query corresponding to a proof term selector. Presently, the effect is the same as noteing a proof term and selecting the noted fact variable. However, having a ProofTerm query would allow us in principle to manage proof terms whose arguments differ across branches.

99.  case class QProofVar(x: Variable) extends ContextQuery with Product with Serializable

    Matches only facts which are bound to fact name x.

    Matches only facts which are bound to fact name x. In the case that x is bound to different facts on different branches, both facts are returned so that they may be (soundly) disjoined.

100.  case class QUnify(pat: Expression) extends ContextQuery with Product with Serializable

     Not to be confused with QUnion.

     Not to be confused with QUnion. Matches all formulas which unify with a given pattern.

101.  case class QUnion extends ContextQuery with Product with Serializable

     Matches all facts matched by at least one of l and r

102.  case class RBranch(l: ContextResult, r: ContextResult) extends ContextResult with Product with Serializable

     When results differed for two parallel branches of a proof, return each branch, distinguished

103.  case class RCF() extends Method with Product with Serializable
104.  case class RStrongFailure(msg: String) extends ContextResult with Product with Serializable

     Strong failures represent an issue that must be reported regardless of what happens on other branches

105.  case class RSuccess(facts: Set[(Option[Ident], Formula)], assigns: Set[Assign] = Set()) extends ContextResult with Product with Serializable

     Collection of facts with optional names, as well as assignments

106.  case class RWeakFailure(msg: String) extends ContextResult with Product with Serializable

     Weak failures only represent that one branch has failed, and so long as some other branch succeeds, we're ok

107.  case class RatIntNum(l: Rational, u: Rational) extends Numeric[RatIntNum, Ternary] with Product with Serializable

     Interval of rational numbers.

108.  case class RatNum(n: Rational) extends Numeric[RatNum, Boolean] with Product with Serializable

     Single rational number.

109.  case class Rational(n: BigInt, d: BigInt) extends Product with Serializable
110.  trait RefinementException extends LocatedException
111.  case class RefinementFailure(s: Statement, g: Program, extraMsg: String = "", node: ASTNode = Triv()) extends LocatedException with RefinementException with Product with Serializable
112.  case class SAssign(x: Ident, f: Term) extends SimpleStrategy with Product with Serializable

     Deterministic assignment.

     Deterministic assignment. Works identically for Angel/Demon.

113.  case class SAssignAny(x: Ident) extends SimpleStrategy with Product with Serializable

     Nondeterministic assignment resolved by demon

114.  case class SChoice(l: AngelStrategy, r: AngelStrategy) extends SimpleStrategy with Product with Serializable

     Demonic choice

115.  case class SCompose(children: List[AngelStrategy]) extends SimpleStrategy with Product with Serializable

     (n-ary) sequential composition, identical for Demon vs Angel.

116.  case class SLoop(s: AngelStrategy) extends SimpleStrategy with Product with Serializable

     Demonic loop

117.  case class SODE(ode: ODESystem) extends SimpleStrategy with Product with Serializable

     Differential equation with decidable domain constraint and Demonic duration

118.  case class STest(f: Formula) extends SimpleStrategy with Product with Serializable

     Demon must pass test f.

     Demon must pass test f. Strategies are weak-test, assume f is decidable

119.  sealed trait Selector extends ASTNode
120.  sealed trait SimpleStrategy extends AngelStrategy

     A simple strategy is one where Angel makes no choices, only Demon

121.  case class Snapshot(m: Map[String, Subscript]) extends Product with Serializable
122.  case class Solution() extends Method with Product with Serializable
123.  sealed trait Statement extends ASTNode
124.  case class Switch(scrutinee: Option[Selector], pats: List[(IdentPat, Formula, Statement)]) extends Statement with Product with Serializable
125.  case class SwitchProgress(switch: Switch, onBranch: Int, progress: Statement) extends MetaNode with Product with Serializable
126.  case class SynthesizeDecl(thmName: Ident) extends KaisarDecl with Product with Serializable

     Display the synthesized strategy resulting from an already-proved proof.

127.  sealed trait Ternary extends AnyRef
128.  case class TernaryNumber[number <: Numeric[number, Boolean]](num: number) extends Numeric[TernaryNumber[number], Ternary] with Product with Serializable
129.  case class TestFailureException(nodeID: Int) extends Exception with Product with Serializable

     Indicates that a Demonic test failed, thus Demon loses

130.  case class TheoremDecl(name: Ident, inPf: Statement, outPf: Statement = Triv(), conclusion: Formula = True) extends KaisarDecl with Product with Serializable

     Check a proof of a strategy and give it a name

131.  case class Time(opt: Boolean) extends OptionSpec with Product with Serializable

     If tracing is also enabled, enabling time will print the cumulative runtime at each line, to allow macro-scale performance measurements.

     If tracing is also enabled, enabling time will print the cumulative runtime at each line, to allow macro-scale performance measurements. The timestamp resets each time this option is enabled, even if it is already on.

132.  case class Trace(opt: Boolean) extends OptionSpec with Product with Serializable

     When tracing is enabled, every proof statement is printed as it is checked, with line numbers

133.  case class Triv() extends Statement with Product with Serializable
134.  case class TuplePat(pats: List[AsgnPat]) extends AsgnPat with Product with Serializable
135.  case class UnknowingFactory[N <: Numeric[N, Boolean]](factory: NumberFactory[Boolean, N]) extends NumberFactory[Ternary, TernaryNumber[N]] with Product with Serializable
136.  case class Unknown() extends Ternary with Product with Serializable
137.  case class UnsupportedStrategyException(nodeID: Int) extends Exception with Product with Serializable

     Indicates that expression was not in the executable fragment

138.  case class Using(use: List[Selector], method: Method) extends Method with Product with Serializable
139.  case class VarPat(x: Variable, p: Option[Ident] = None) extends AsgnPat with Product with Serializable
140.  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

     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

141.  case class Was(now: Statement, was: Statement) extends MetaNode with Product with Serializable
142.  case class While(x: IdentPat, j: Formula, s: Statement) extends Statement with Product with Serializable
143.  case class WhileProgress(whilst: While, progress: Statement) extends MetaNode with Product with Serializable
144.  case class WildPat() extends AsgnPat with Product with Serializable
145.  class WrappedDemonStrategy[number <: Numeric[number, Ternary]] extends DemonStrategy[number]

     Produces an executable DemonStrategy from high-level BasicDemonStrategy interface, fit for use with SimpleStrategy.apply.

     Produces an executable DemonStrategy from high-level BasicDemonStrategy interface, fit for use with SimpleStrategy.apply. The major contribution is that WrappedDemonStrategy automatically remembers the Angelic choices from the ambient Angelic strategy, and makes Demon simulate those Angelic choices automatically, leaving you to implement only the true Demon operations.