Expressions
HeyVL expressions can be used inside specifications and statements and evaluate to values in some program state.
Expression Syntax
The syntax of expressions (Expr
) consists of the following parts:
- Quantifiers:
inf Ident: Type, Ident: Type. Expr
sup Ident: Type, Ident: Type. Expr
forall Ident: Type, Ident: Type. Expr
exists Ident: Type, Ident: Type. Expr
- Quantifier annotations such as triggers are also allowed, e.g.
forall Ident: Type @trigger(Expr). Expr
- Boolean Operators (returning type
Bool
):- Logical And:
Expr && Expr
- Logical Or:
Expr || Expr
- Equals:
Expr == Expr
- Less Than:
Expr <= Expr
- Not Equals:
Expr != Expr
- Greater Or Equals:
Expr >= Expr
- Greater:
Expr > Expr
- Logical And:
- Binary Lattice and Heyting Algebra Operators (on types
Bool
andEUReal
):- Binary Minimum/Infimum:
Expr ⊓ Expr
orExpr \cap Expr
- Binary Maximum/Supremum:
Expr ⊔ Expr
orExpr \cup Expr
- Implication:
Expr → Expr
orExpr ==> Expr
- Coimplication:
Expr ← Expr
orExpr <== Expr
(note that this is not just a flipped version of the implication→
, but rather its lattice-theoretic dual!) - Comparison:
Expr ↘ Expr
- Cocomparison:
Expr ↖ Expr
- Binary Minimum/Infimum:
- Arithmetical Operators (c.f. number types):
- Addition:
Expr + Expr
- Subtraction/Monus:
Expr - Expr
- Multiplication:
Expr * Expr
- Division:
Expr / Expr
- Modulo:
Expr % Expr
- Addition:
- Other Expressions:
- Let Expressions:
let(Ident, Expr, Expr)
- If-Then-Else Expressions:
ite(Expr, Expr, Expr)
- Function Calls:
Ident(Expr, ..., Expr)
- Negation:
!Expr
- Conegation:
~Expr
- Embed:
?Expr
(usually written with parentheses:?(Expr)
) - Iverson:
[Expr]
- Parentheses:
(Expr)
- Let Expressions:
- Literals:
- String Literals: text enclosed by
"
characters (regular expression:"[^"]*"
). Note that Caesar does not support a properString
type yet. - Integers: given by regular expression
[0-9]+
(default type:UInt
) - Decimals: given by regular expression
[0-9]+\.[0-9]+
(default type:UReal
) - Boolean Constants:
true
andfalse
- String Literals: text enclosed by
- Identifiers (
Ident
): Names of things, from the language of the regular expression[_a-zA-Z][_a-zA-Z0-9']*
.
Types (Type
) are types from Caesar's standard library and user-defined types from domains.
The above list is presented roughly in order of operator precedence. Note that we plan to change some operator precedences, so when in doubt, use more parentheses to guarantee the correct interpretation.
The most precise grammar specification can be found in Caesar's source code (src/front/parser/grammar.lalrpop
).
Semantics and Under-Specified Expressions
In our paper on HeyVL (cf. Section 2), we give a formal semantics for HeyLo, our logic for reasoning about expected values.
HeyLo includes operators such as ==>
, <==
, !
, ~
, ?(e)
, and more.
Caesar's expressions are a superset of HeyLo.
In particular, the paper explains in detail the lattice and Heyting algebra operators that Caesar supports.
Note that some operations are not fully specified (under-specified).
The division and remainder operators (Expr / Expr
and Expr % Expr
) are not fully defined for all values.
Caesar translates these operators directly to SMT, where the SMT solver may assign arbitrary interpretations to e.g. divisions by zero.
You can find more information in the Z3 documentation on division.
The -
operator is always fully defined in Caesar.
On unsigned types such as UInt
, it corresponds to monus, i.e. truncating subtraction that is always at least 0
.
On signed types such as Int
, it corresponds to the usual subtraction.
If-Then-Else
The ite
built-in function allows to choose one of two expressions based on the result of a Boolean expression.
For example:
var x: UInt = ite(true, 32, 64);
The first parameter is the Boolean expression.
If it evaluates to true
, the result of evaluating the second expression is returned.
Otherwise, the third expression is evaluated.
Let Expressions
let
expressions enable the declaration of local variables within an expression.
For example:
var x: UInt = let(b, true, ite(b, 32, 64));
The let
expression creates a new local variable b
and sets its value to true
.
This variable b
is available within the let
expression's third argument.
In contrast to variable declaration statements using var
, let
expressions do not require type annotations.
The type of the variable is inferred from the second expression.
Quantifiers
HeyVL features Boolean and quantitative quantifiers: forall
, exists
, inf
, sup
.
For example:
forall x: Int, y: UInt. x == y || x != y
Triggers
We also support triggers for the Boolean quantifiers via annotations. They are patterns that will instruct the SMT solver to instantiate quantifiers if the pattern is found in the current list of terms it maintains. For example:
forall list: []Int @trigger(len(list)). len(list) >= 0
Multi-patterns are also supported, by writing a comma-separated list inside the @trigger
annotation:
forall list: []Int @trigger(len(list), len(list)). len(list) >= 0
For more information on how triggers/patterns work in general, see the Z3 User Guide and the Dafny documentation.
Relative Completeness
Caesar's expression syntax is based on the expressive assertion language for probabilistic verification by Batz et al. In theory, expressiveness means that for many programs and properties, we know that we can express all pre-expectations and invariants in the expression syntax when a post-expectation is written in that syntax.
Formally, we have that the weakest pre-expectation calculus wp
is relatively complete with respect to this language, which means that wp[P](post)
is effectively constructible for all programs P
and expectations post
in their syntax.
Their syntax includes enough constructs to specify many interesting properties, such as termination probabilities or the distribution over final states, even including stuff like harmonic numbers. See the paper's Section 12 for more details.
Of course, this does not mean that all of these verification problems are decidable.
It just means that in theory, the undecidable part is only in the final inequality check pre <= wp[P](post)
instead of the computation of wp[P](post)
.
The section on SMT theories and incompleteness specifies which of these inequalities are actually decidable with Caesar.
SMT Theories and Incompleteness
Expressions are the main reason for incompleteness of Caesar, i.e. instances Caesar is unable to decide whether a given HeyVL program verifies or not. Caesar's incompleteness comes from incompleteness of the underlying SMT solver which is used to prove or disprove verification.
At the moment, Caesar's translation of HeyVL verification problems is rather direct: most expressions are translated as one would intuitively expect. If operators have a direct correspondence in SMT-LIB, then we translate directly to those. Otherwise, usually only additional simple case distinctions are introduced. We have some more explanations in Section 5 of our paper on HeyVL.
As a consequence, it is usually pretty simple to predict which SMT-LIB theories will be used for the SMT query done by Caesar. Also refer to the Z3 documentation on arithmetic theories, since a lot of Caesar's reasoning will need arithmetic.
Here are some rules of thumb for (in-)completeness:
- Linear integer and real arithmetic (QF_LRA, QF_LIRA) is decidable.
- Nonlinear integer arithmetic (QF_NIA) is undecidable.
- Nonlinear real arithmetic (QF_NRA) is decidable for algebraic reals.
- Quantifiers usually introduce undecidability, although there are a bunch of strategies and fragments in Z3 that allow decidability.
- In particular, restrictive quantifier triggers can help e-matching prove many instances.
- HeyVL's quantitative quantifiers (
inf
andsup
) currently have a very naive default encoding that is problematic for Z3. If the quantitative quantifiers cannot be eliminated by Caesar's quantifier elimination (QE) procedure, then they are often a cause of nontermination of Caesar.- Quantitative quantifiers also come from the semantics of
havoc
andcohavoc
. However, for e.g. the induction-based proof rules, the HeyVL encodings fall into a fragment where Caesar's QE applies and the generated quantifiers are eliminated.
- Quantitative quantifiers also come from the semantics of
- In practice, the SMT solver can often prove correctness, but it often has problems with refutations (i.e. providing counter-examples).