KeYmaera X Syntax and Informal Semantics

Syntax for Differential Dynamic Logic

KeYmaera X uses a slightly different syntax for dL from the presentation given in lectures and papers. This is in order to more closely match the syntax used by common programming languages and make it easier to parse. As usual, the syntax is divided into terms, formulas, and hybrid programs.

For more detail, see KeYmaera X Tutorial

Syntax by Example

The KeYmaera X syntax for basic formulas in real arithmetic, such as

x > 1/2 & y >= 0 -> x+y > 1/2

allows for

• real-valued variables such as x and y,
• number literals such as 1 (decimal numbers such as 0.5 are syntactic sugar and translated by the parser to rationals like 1/2),
• arithmetic operations such as sum x+y and division 1/2 with the usual operator precedence,
• comparisons such as greater > and greater-or-equal >=, and
• connectives such as conjunction & and implication ->.

  Note that conjunction & binds strongest, disjunction | next, implication -> and bi-implication <-> bind weakest. So, x>1/2 & y>=0 -> x+y>1/2 is equivalent to (x>1/2 & y>=0) -> x+y>1/2, but not to x>1/2 & (y>=0 -> x+y>1/2).

Formulas about the behavior of hybrid programs are expressed with modal operators [] and <>

x>0 -> [{ x := x+1; ++ y := *; ?y>=0; x := x+y; }*]x>0

with programs

• Assignment such as x := x+1; which sets the value of x to the value of the term x+1, so increments x by 1
• Nondeterministic assignment such as y := *;, which sets the value of y to any real value
• Tests such as ?y>=0;, which succeeds when formula y>=0 is true and fails otherwise, so here tests that the nondeterministically chosen value of y is non-negative
• Sequential composition a; b which executes a hybrid program a and if a succeeds then executes hybrid program b on the result of a.
• Nondeterministic choice a ++ b which executes either hybrid program a or hybrid program b.

  Note that sequential composition ; binds stronger than nondeterministic choice ++, so x:=1;y:=x; ++ y:=-x; is the same program as {x:=1;y:=x;} ++ y:=-x;}, but different from x:=1; {y:=x; ++ y:=-x;}.

Additionally to the traditional discrete program operators illustrated above, hybrid programs can mention differential equations as follows.

x>2 -> [{ y := *; {x'=y, y'=2 & x>1} }*]x>0

• Primes such as x' denote the derivative of x with respect to time.
• The differential equation system x'=y, y'=2 & x>0 consists of two simultaneously evolving differential equations x'=y where x evolves with slope y, and y'=2 expresses that y evolves with constant slope 2.
• The evolution domain constraint x>1 separated from the differential equations with & expresses that all continuous behavior described by the differential equations stays inside the region x>1, so the evolution stops anytime before x>1 becomes false.

Term Syntax

Formally, the term syntax is the grammar summarized here:

TERM ::= x | r | TERM OP TERM | (THETA)' | f(args)

• x is a program variable, which is subtly different from a constant symbol. Syntactically, x doesn't have any parentheses. (Advanced material) What are the other differences? Program variables get overwritten by programs and quantifiers, but constants do not. Constants can be replaced with arbitrary terms using substitution, but program variables can't. (Most of the time, substitution happens behind the scenes, but if for example you are extending KeYmaera X, this will be helpful to know). Since one of the things you can replace x() with is just x, they are in this sense more general.

  So in short, use x if you need to overwrite a variable, x() if you don't. Even if you don't need to use substitution, this is a good way to tell the reader the value won't change.

  Exercise Does there exist an x such that x()>0: exists x. x() > 0. Or in other words, is the formula valid? Why so?

• r ∈ Q is a literal constant. Examples are 0, 1., and 3.1415. r must be a rational, so 2/3 is okay but pi and sqrt(2) are not. You could think of these as interpreted constant symbols: each number always has the same interpretation: itself

• TERM OP TERM Where each TERM is arbitrary (and they don't have to be the same as each other). OP can be any of the built-in arithmetic operators:

  • addition +
  • multiplication *
  • subtraction - (unary minus also supported)
  • division /. Any time you divide, make sure you don't divide by zero!
  • exponentiation ^. You can exponentiate arbitrary terms, with two caveats. If the exponent contains variables/functions, KeYmaera X is very unlikely to prove anything about it automatically. If you use fractional exponents (e.g. if you take a square root x^(1/2)), you must make sure you never use them on negative numbers!

• Differential terms (TERM)' are the derivative of TERM. What does this actually mean (what are the semantics)? When (TERM)' appears after an ODE, the meaning should be intuitive, since the derivative is given meaning by the ODE.

  What if you're not inside an ODE, or if there's an assignment [x' := TERM] after the ODE? In this case you could make sense of (TERM)' as following all the equations for derivatives, like (TERM1 + TERM2)' = (TERM1)' + (TERM2)'. If you apply all the equations, you'll get down to just differential symbols x' (see next bullet).

  Even this definition is messier than we would like, so instead we actually define (TERM)' as the sum of partial derivatives of TERM with respect to every program variable. This definition is equivalent, but cleaner.

• (TERM) You can add parentheses around any subterm to affect parsing order. For complex terms, sometimes parentheses help readability if the term already parses correctly but it's
  not obvious to the reader. Just don't go overboard and put them everywhere :-)

• f(args) is a function, applied to the arguments args.

Functions come in a few flavors: 1 Interpreted functions are functions that mean something special. As of this writing the only interpreted functions are min, max, and abs, which take exactly two arguments and have their standard meanings. These functions can be useful for advanced proofs. They are generally not needed in simple proofs such as course labs. 2 (Advanced material) Uninterpreted functions are functions that don't mean anything specific. All other functions are in this category, e.g. f(x), g(y), reticulate(spline). Because we don't know what function it is, when we prove something about f(x), we're proving that it's true no matter what f is, so the proof can't assume anything about f. Uninterpreted functions should not come up when proving things about a specific model, but if you ever try to prove your own axioms or proof rules, they can be useful. Within uninterpreted functions there is another class special enough to deserve its own mention. 3 (Advanced material) Constant symbols (e.g f(), c()) are uninterpreted function symbols with no arguments. These stand for unknown real numbers (i.e. they are always universally quantified). Use these in your models for values that should never change. They will also be introduced sometimes when you run a proof step in KeYmaera X.

Exercise:

• Is the maximum of two values x(),y() equal to x() or equal to y() in all states? max(x(), y()) = x() | max(x(), y()) = y()
• Is the derivative of e()^x() equal to itself in all states according to the interpreted functions known to KeYmaera X? (e()^x())' = (e()^x())
• Is the Pythagorean identity cos(x())^2 + sin(x())^2 = 1 true in all states? Is it true in all states according to the interpreted functions known to KeYmaera X?
• Is the following formula true in all states (valid)? Is it satisfiable in some states? i()^2 = -1
• Is E() equal to m()*c()^2 in all states? Is it satisfiable in some states? E() = m()*c()^2

Formula Syntax

Formally, the formula syntax is in the grammar summarized here:

FORMULA ::= 
   true | false  | "FORMULA | FORMULA" 
 | !FORMULA | FORMULA & FORMULA 
 | FORMULA -> FORMULA | FORMULA <-> FORMULA
 | TERM = TERM | TERM > TERM | TERM >= TERM 
 | TERM < TERM | TERM <= TERM 
 | \forall x FORMULA | \exists x FORMULA
 | [HP]FORMULA | <HP>FORMULA
 | (FORMULA)
 (Advanced material)
 | p(args) |C(FORMULA)

• true and false are always true and always false, respectively

• |, !, &, ->, and <-> are the standard classical propositional connectives or, not, and, implies, and equivalence.

• =, >, >=, <, <= are standard comparison operators on the reals

• Boxes [HP]FORMULA and diamonds <HP>FORMULA are modal formulas with the meaning that [HP]FORMULA is true if FORMULA is true after all possible executions of HP and <HP>FORMULA is true if FORMULA is in true in at least one execution.

  We use boxes to prove safety properties, like "the car never hits the other car". Diamonds, on the other hand, can be used to prove liveness properties, like "the car eventually gets to the destination, but I don't know how long it will take"

• \forall, \exists are quantifiers over real numbers. They behave as standard in first-order logic. They always quantify over program variables, never constant symbols.

• (FORMULA) You can add parentheses around any subformula to affect parsing order. For complex formulas, sometimes parethesis help readability if the formula already parses correctly but it's
  not obvious to the reader. Just don't go overboard and put them everywhere :-)

(Advanced Material)

• p(args) is an uninterpreted predicate symbol: a predicate (i.e. boolean-valued function) that depends only on the real-valued arguments args. Unlike with functions, there are no interpreted predicate symbols, though true and false could be understood as nullary predicate symbols and the comparison operators <, <=, =, >=, > can be understood as binary predicate symbols. Predicate symbols only take reals as arguments.

• C(FORMULA) is a unary predicational symbol (also known as a quantifier symbol). Unlike a predicate symbol, it takes a formula as an argument. It is best understood as a function from formulas to booleans, not from booleans to booleans. Why is that, you ask? A function from booleans to booleans would only be allowed to see the value of FORMULA in the current state, but predicationals have the magic power of looking at other states by inserting quantifiers around the formula. For example, the following is a valid proof:

  -------------------------------
  (y^2 > x^2) <-> abs(y) > abs(x)
  ------------------------------------------------------------------------
  (\forall x \exists y y^2 > x^2) <-> (\forall x \exists y abs(y) > abs(x))
  

Where here C(p()) = \forall x \exists y p()

Hybrid Program Syntax

Formally, a hybrid program is in the grammar summarized here:

HP ::= 
  x := TERM;
| x := *;
| ?FORMULA;
| HP HP
| HP ++ HP
| HP*
| x' = TERM, .... & FORMULA
| {HP}

• Assignment x := TERM assigns the current value of TERM to x, which can be either a program variable or differential symbol.

• Nondeterministic assignment x := * overwrites x nondeterministically with any real value. Inside a box (e.g [x := *;]x > 0) this means we don't get to pick x and have to assume it could be anything, so [x := *;]x > 0 is false because sometimes x is -1. Inside a diamond, we get to pick x, so <x := *;>x > 0 is true because we can pick x = 1.

• Tests ?FORMULA fail if FORMULA is false, else do nothing. FORMULA can be any formula, but is most often first-
  order logic (usually doesn't contain programs).

• Sequential Composition HP HP of two programs HP1 HP2 runs HP1 then runs HP2 in the resulting state. Note this is different from the lecture/paper presentation, where this would be HP1; HP2. Instead ; is a terminator in the KeYmaera X presentation, appearing after every assignment and test.

  For 15-424 students: We will not test you on silly syntax details, at least not on purpose. The reason for going into all this detail is to make you less confused if you're having trouble writing a model that parses. See the examples/exercises after this section for more help.

• Nondeterministic Choice HP ++ HP of two programs HP1 ++ HP2 nondeterminstically chooses to run either HP1 or HP2.

• Nondeterministic Iteration HP* nondeterministically runs HP any finite number of times (including 0).

• ODE Evolution x' = TERM, .... & FORMULA evolves the system of differential equations consisting of all the x' = TERM for a nondeterministic length of time (including 0), so long as FORMULA holds true everywhere throughout the
  evolution. Note that there is no semicolon.

  If you want two domain constraints, you just make FORMULA a conjunction. Now there's two &s but they mean different things: one connects an ODE to its domain, the other is conjunction:

  e.g. {x' = v, v' = a & v >= 0 & x >= 0} parses as {x' = v, v' = a & (v >= 0 & x >= 0)}

  When the domain (and ampersand) is omitted it is implied to be true

  (Advanced Material) ODE systems can also contain differential program constants (usually named c) which range over arbitrary systems of equations and can be instantiated by substitution. This is primarily used to define axioms which work for systems of any size. e.g. [c & P]P says that the domain constraint holds after an ODE no matter what ODE it is.

• {HP} Curly brackets are the parentheses for programs, by analogy with Algol-like languages (or "C" and "Java" as the kids say nowadays). You'll notice that the above ODE system uses brackets. To ensure correct parsing, ODE systems often need brackets around them. It will serve you well to make that a habit.

Examples: Three choices, each is two assignments:

  {x := 0; y := 0;}
++{x := 0; y :=*;}
++{x := *; y :=*;}

Composition of two choice operators, each chooses between two assignments: {x := 0; ++ x := 1;}{y := 0; ++ y := 1;}

Sequential composition of two ODEs {x' = 1}{y' = 2}

System of two ODEs {x' = 1, y' = 2}

Assignment, then ODE, then assignment t := 0; {t' = 1 & t < 5} x := t^2;

Syntax for Model Files

When we want to prove a model in KeYmaera X, we first have to write it as a .kyx file.

ARCHIVE ::= ARCHIVEENTRY+

ARCHIVEENTRY ::= ENTRYKIND "STRING" (DEFINITIONS | PROGRAMVARIABLES)* PROBLEM TACTIC* End.

ENTRYKIND ::= ArchiveEntry | Theorem | Lemma | Exercise

DEFINITIONS ::= Definitions (FUNCDEF | PREDDEF | HPDEF)+ End.
FUNCDEF ::= Real f(args); | Real f(args) = (TERM);
PREDDEF ::= Bool p(args); | Bool p(args) <-> (FORMULA);
HPDEF   ::= 'HP' prg ::= {HP};

PROGRAMVARIABLES ::= ProgramVariables PROGVARLINE+ End.
PROGVARLINE ::= Real x (, x)*;

PROBLEM ::= Problem FORMULA End.

TACTIC ::= Tactic "STRING" TAC End.

A .kyx file has three parts:

• Definitions (optional): This includes constants, functions, predicates, and program abbreviations used in the model. Most simple models don't need any functions (and only a few interpreted functions are supported). Therefore the main purpose of the Definitions part is to express constants: values that are arbitrary but should never change throughout the execution of your model.

  Example:

  Definitions
    /* Builtin interpreted functions need no definition, supported: abs(Real), min(Real,Real), max(Real,Real) */
    Real A;
    Real B;
    Real succ(Real x) = ( x+1 );      /* Function abbreviation succ will be expanded, succ(x) to x+1 and succ(z) to z+1 */
    Bool gt(Real x, Real y) <-> ( x>y );  /* Predicate abbreviation gt will be expanded, gt(x,y) to x>y, gt(a,b) to a>b */
    HP inc ::= { x:=x+1; };               /* Program abbreviation inc will be expanded to x:=x+1 everywhere in the model */
  End.
  

  Real is the name for the type of real numbers. All constants and variables in KeYmaeraX are real numbers, but for functions we can use the above syntax to express the number of arguments (two for max). Bool is the name for the type of boolean predicates, HP the type of hybrid programs.

• ProgramVariables specifies all the mutable variables in the model:

  Example:

  ProgramVariables
    Real x;
    Real v;
    Real a;
  End.
  

• Problem specifies the formula you want to prove.

  Example:

  Problem
    x = 0 & A > 0 & B > 0 -> [{a := A; ++ a := B;}{x' = v, v' = a}]x >= 0
  End.
  

Putting the sections together, a complete model might look like:

Definitions
  Real A;
  Real B;
End.

ProgramVariables
  Real x;
  Real v;
  Real a;
End.

Problem
  x = 0 & A > 0 & B > 0 -> [{a := A; ++ a := B;}{x' = v, v' = a}]x >= 0
End.

Using abbreviations, the above example can be rephrased like:

Definitions
  Real A;
  Real B;
  Real low() = ( 0 );
  Bool init(Real x) <-> ( x = low() & A > 0 & B > 0 );
  Bool safe(Real x) <-> ( x >= low() );
  HP ctrl   ::= { a := A; ++ a := B; };
  HP motion ::= { {x' = v, v' = a} };
End.

ProgramVariables
    Real x;
    Real v;
    Real a;
  End.

Problem
  init(x) -> [ctrl;motion;]safe(x)
End.

Design Annotations in the Model File

Additional design insight, such as loop invariants and differential invariants, can be annotated in the model with @invariant annotations.

  Definitions
    Real A;
    Real B;
  End.

  ProgramVariables
    Real x;
    Real v;
    Real a;
  End.

  Problem
    x = 0 & A > 0 & B > 0 -> 
    [{
       {a := A; ++ a := B;}
       { {x' = v, v' = a}@invariant(v>=old(v), x>=old(x)) }
     }*@invariant(x>=0)
    ]x >= 0
  End.

The reserved function old(x) refers to the initial value of x at the start of the ODE.

Multiple Entries in a Model File

KeYmaera X files can have multiple named entries, each with (optional) tactics to prove the entry.

ArchiveEntry "Increment in a loop"

ProgramVariables
  Real x;
End.

Problem
  x>0 -> [{x:=x+1;}*@invariant(x>0)]x>0
End.

Tactic "Automated proof"
  master; done
End.

End.

ArchiveEntry "Continuously evolve forward"

ProgramVariables
  Real x;
End.

Problem
  x>0 -> [{x'=1}]x>0
End.

Tactic "Automated proof"
  master; done
End.

Tactic "Manual proof with solve"
  implyR(1); solve(1); QE; done
End.

Tactic "Manual proof with differential invariant"
  implyR(1); dC("x>=old(x)",1); <(
    dW(1); QE; done
    ,
    dI(1); done
  )
End.

End.

Syntax for Tactics (Bellerophon)

In KeYmaera X, we can write programs to do proofs for us, called tactics. KeYmaera X will also generate a tactic for you any time you do a proof step, so for beginners we recommend reading and copy/pasting tactics produced by KeYmaera X before writing your own.

Syntax for tactics:

TAC ::= builtin(ARGS)
       | expand "NAME"
       | expandAllDefs
       | TAC; TAC 
       | "TAC | TAC" 
       | ?TAC
       | (TAC)* 
       | <(TAC, ..., TAC) 
       | <("LABEL_1": TAC, ..., "LABEL_n": TAC)
       | TAC using LIST
       | nil

• builtin(ARGS) Builtin tactics do all the hard work, the other kinds of tactics just combine builtin tactics. These include all the sequent calculus and hybrid program rules. Some builtin tactics, such as master and QE, work on the entire sequent and so don't need any arguments.

  Most builtins take exactly one argument telling you what formula to use it on. Conclusions are positive numbers, starting with 1. Assumptions are negative numbers, starting with -1. If you want to work on a subformula, you can use dot notation to specify the subformula. for example if you have ((A & B) -> C) as formula 1, then 1.0 is (A & B), 1.0.0 is A, 1.0.1 is b and 1.1 is C

  A few tactics like allL and loop take a term or formula as an argument. When you pass a formula or term to a tactic as an argument, you enclose it in double quotes, e.g. we could call loop like loop("x > 0", 1)

• expand "NAME" and expandAllDefs expand definitions

• TAC1; TAC2 Runs TAC1 first and then TAC2, but only if TAC1 succeeds

• TAC1 | TAC2 Runs TAC1 first and if it fails, it tries TAC2 instead. This is really useful when you want to write some reusable proof search program (e.g. your own custom version of master), but is less often used if you're just trying to do one specific proof about one specific model.

• ?TAC tries running TAC, and if TAC fails, it ignores the failure and succeeds but does nothing. This is useful in search programs if there's some step that might not work all the time.

• (TAC)* runs TAC over and over again until it can't run TAC any more. This is useful when writing proof search programs and also useful for repeating simple repetitive proof steps. For example, if you have a bunch of &s in your assumptions that you want to break apart, you could do something like (andL('L)*)

• <(TAC1, ..., TACN) Runs each tactic TAC_i on the i'th subgoal. It fails immediately if there are not exactly i subgoals. You will typically see this immediately after some tactic that causes the proof to branch, such as andR or orL --- most tactics assume they are working on an individual subgoal and so will not work after an andR or orL without branching.

• <("LABEL_1": TAC1, ..., "LABEL_N": TACN) Runs each tactic TAC_i on the subgoal with label LABEL_i.

• TAC using LIST Runs tactic TAC on a sequent that includes only formulas from LIST of formulas fml_1 :: ... :: fml_n :: nil.

• nil is a builtin tactic that does absolutely nothing, but succeeds. This is used a lot in the tactics autogenerated by KeYmaera X any time the syntax says it has to write down a tactic but it doesn't want to do anything. For example if you call a branching tactic but only do work on the first branch, the remaining branches will have the nil tactic.