PVL Syntax Reference

On this page you can find a description of the specification language of VerCors. In general, the specification language extends the language that is verified, like Java. That means that all types, (pure) operators, etc. from the source language can also be used in the specifications, together with the specification-only constructs described below.

Additionally, this page describes PVL, the Prototypal Verification Language. It is a language similar to Java or C and can be verified like them, so the same specification constructs are available. However, it is developed specifically for VerCors, so we also provide the information that is usually found in the language documentation, like the C standard.

General

• Specifications are usually embedded in JML-like comments: /*@ spec @*/ or //@ spec line. Exception: In PVL, specifications are not embedded in comments, instead they are written into the code directly.

• In PVL, identifiers can consist of the characters a-z, A-Z, 0-9 and _. However, they must start with an underscore or letter (a-z, A-Z).

  In specifications, the same rules apply for identifiers as in the language that is specified, e.g. Java identifiers in specifications of Java.

  Note that the following words are reserved and can therefore not be used as identifiers: create, action, destroy, send, recv, use, open, close, atomic, from, merge, split, process, apply, label, \result, write, read, none, empty and current_thread. However, keywords can be wrapped in backticks, to turn them into identifiers, e.g. create cannot be used as an identifier, but `create` is an identifier.

• Most specification constructs are self-contained statements, like preconditions, loop invariants or ghost assignments. Those end with a semicolon ;. However, a few elements, like with side conditions, are parts of another statement, and do not have their own semicolon.

PVL

• At the top level of a program, there can be methods directly (like in C). But more commonly, those are defined within a class:

class ClassName {
    // Here you can add any constructors, class variables and method declarations
}

• The keyword this is used to refer to the current object, null for the null reference ("pointer to nothing").
• You can write single-line or multi-line comments as follows:

// This is a single-line comment
/* 
    This is a 
    multi-line comment 
*/

• Like in C or Java, statements in PVL should end with a semi-colon ;.
• For a more detailed description, see https://github.com/utwente-fmt/vercors/wiki/Prototypal-Verification-Language

Types and Data Structures

The following table lists the basic and composed data types supported in the specification language.

Type	Description
resource	Boolean-like type that also allows reasoning about permissions. See https://github.com/utwente-fmt/vercors/wiki/Predicates
frac	Fraction, used for permission amounts. See https://github.com/utwente-fmt/vercors/wiki/Permissions
zfrac	Fraction that can also be zero.
rational	Unbounded rational number
bool	Boolean value that is either true or false
string	Text, i.e. a string of characters
ref	Reference to an object, similar to Viper's Ref type. Mostly for internal usage, e.g. ADT definitions.
process	Type of actions and defined processes in process algebra models. See https://github.com/utwente-fmt/vercors/wiki/Process-Algebra-Models
any	Artificial type that is a supertype of any other type. Mostly for internal usage, e.g. rewrite rules.
nothing	Artificial type that is a subtype of any other type. Mostly for internal usage, e.g. rewrite rules.
seq<T>	Defines an immutable ordered list (sequence). T should be replaced by a type. See https://github.com/utwente-fmt/vercors/wiki/Axiomatic-Data-Types
set<T>	Defines an immutable orderless collection that does not allow duplicates ("set"). T should be replaced by a type. See https://github.com/utwente-fmt/vercors/wiki/Axiomatic-Data-Types
bag<T>	Defines an immutable orderless collection that does allow duplicates ("bag" or "multiset"). T should be replaced by a type. See https://github.com/utwente-fmt/vercors/wiki/Axiomatic-Data-Types
map<T1, T2>	Defines an immutable orderless collection of key/value pairs that does not allow duplicate keys ("map", "record" or "dictionary"). T1 and T2 should be replaced by Types. See https://github.com/utwente-fmt/vercors/wiki/Axiomatic-Data-Types
option<T>	Extends type T with an extra element None. Each element is then either None or of the style Some(e) where e is of type T. T should be replaced by a type. Options cannot be unpacked at the moment. See https://github.com/utwente-fmt/vercors/wiki/Axiomatic-Data-Types
tuple<T1,T2>	Defines a pair, where the first entry is of type T1 and the second of type T2. Can be nested to create larger tuples. See https://github.com/utwente-fmt/vercors/wiki/Axiomatic-Data-Types
pointer<T>	Defines the type of a pointer to an element of type T. T should be replaced by a type. See https://github.com/utwente-fmt/vercors/wiki/Arrays-and-Pointers
type<T>	Used to define type variables that are subtype of T. Mostly used for rewrite rules, e.g. (\forall type<any> T; (\forall T t; expr))
either<T1, T2>	Defines the type of an object o that is either of type T1 or of type T2. See TODO
language type	A type from the base language, e.g. Java, can also be used in the specifications for that language. This usually provides basic types like int.

PVL

In PVL, the specification types above can also be used in the regular program. Additionally, the following types are available:

Type	Description
int	Integer
boolean	true or false
void	Used when a method does not return anything
float32	32-bit floating point number (Note: support still limited)
float64	64-bit floating point number (Note: support still limited)
char	Character
T[]	Array which contains elements of type T. T should be replaced by a type. Note that when you initialize a new array, you should always define the length of the array, e.g. new int[3] instead of new int[].

Expressions

Operators

Code	Description
\	Division that creates a frac, rather than integer rounding. Same precedence as multiplication and division.
==>	Logical implication. The left side should be boolean-typed, the right side boolean or resource. Lower precedence than disjunction ||. See https://github.com/utwente-fmt/vercors/wiki/Specification-Syntax
**	Separating conjunction. a ** b denotes that a and b point to different variables on the heap and that both expressions must evaluate to true. This is used to reason about multiple resources. Same precedence as conjunction &&. See https://github.com/utwente-fmt/vercors/wiki/Permissions
-*	"Magic wand" or "separating implication". Same precedence as implication ==>. See https://github.com/utwente-fmt/vercors/wiki/Magic-Wands
[p]pred(<args>)	[p] before a predicate invocation scales all permissions in pred by a factor of p. See https://github.com/utwente-fmt/vercors/wiki/Predicates
Left(e)	// unclear. Seems related to type "either" TODO
Right(e)	// unclear. Seems related to type "either" TODO
?.	o?.m(<args>) is a conditional invocation of method m, equivalent to o!=null ==> o.m(<args>). See https://github.com/utwente-fmt/vercors/wiki/Specification-Syntax
m() given {a=b, c=d}	Invokes method m with expression b as value of ghost parameter a and similar for c and d. See https://github.com/utwente-fmt/vercors/wiki/Specification-Syntax
m() yields {a=b, c=d}	Invokes method m, and storing ghost return value b in a and similar for c and d. See https://github.com/utwente-fmt/vercors/wiki/Specification-Syntax
with	augment an expression with a side effect to happen before evaluating it, e.g. /*@ with specInit(); @*/ init(). Previously used for ghost parameters, now obsolete (?) // TODO
then	augment an expression with a side effect to happen after evaluating it, e.g. init() /*@ then specInit(); @*/. Previously used for ghost return values, now obsolete (?) // TODO
(\let T t = exprA; exprB)	Evaluates exprB, replacing every occurence of t with the result of evaluatingexprA. The surrounding parentheses ( ) are required.

ADTs

Axiomatic Data types have several dedicated operators. Some also have corresponding functions, e.g. s1.subsetOf(s2) for s1 <= s2. There are also functions that do not have an operator equivalence, e.g. xs.removeAt(i). See https://github.com/utwente-fmt/vercors/wiki/Axiomatic-Data-Types for the full list.

Code	Description
+	Sequence concatenation, Set union, Bag union
-	Set difference, Bag difference
*	Set intersection, Bag intersection
<, <=	strict subset, or subset-or-equal, respectively (also for bags)
xs[k]	Sequence indexing: kth element of sequence xs; Map indexing: value associated with key k
::	x :: xs prepends element x to the front of sequence xs.
++	xs ++ x appends element x to the end of sequence xs. // Note: Discouraged, support may get removed.
e[l .. r]	Range indexing of sequence e (slicing). Creates a new sequence with the elements of e between indices l (incl.) and r(excl.). One of l or r may be omitted.
e[k -> v]	Updating of map e at index k to new value v (not in-place).
|xs|	Cardinality of collection xs, e.g. length of sequence, size of set.
\values(e1, e2, e3)	create a sequence that stores the values from array e1 between indices e2 and e3.
Some(e)	Turns expression e of type T into an expression of type option<T> containing e.
seq<T>{vals} or [vals]	sequence literal containing values vals (of type T).
set<T>{vals} or {vals}	set literal containing values vals (of type T).
bag<T>{vals} or b{vals}	bag literal containing values vals (of type T).
map<T1, T2>{k1->v1, k2->v2,...}	map literal mapping k1 (of type T1) to v1 (of type T2), etc.
tuple<T1, T2>{v1, v2}	tuple literal containing the two values v1 (of type T1) and v2 (of type T2).
[t: T], {t: T}, b{t: T}	literal describing the empty seq<T>, set<T> and bag<T>, respectively. Note that T is a type parameter that should be replaced with the appropriate type, while t: is part of the syntax and should occur literally, e.g. int[] emp = [t: int];.
{l .. r}	Literal of type seq<int> describing the integer range from l (incl) to r (excl).
set<T>{ e | selectors ; filter }	Set comprehension, creating set that contains expressions of the form e (of type T), based on the variables defined in selectors if they match filter expression filter. Note the restrictions described at https://github.com/utwente-fmt/vercors/wiki/Axiomatic-Data-Types.
x \in xs	Membership check if element x is contained in collection xs. Note: For bags, it returns the number of occurrences, not a boolean.
(\sum int idx; range; e)	Sequence summation: sum expression e (which depends on the index idx) for all indices within the given range. Note: currently not supported.

PVL

Code	Description
==, !=	Equals and not equals for reasoning about the equality of expressions
&&, ||, !	And, or, and negation respectively for reasoning with boolean expressions
<, <=, >, >=	Smaller-than, smaller-or-equal, greater-than and greater-or-equal, respectively, for comparing numerical expressions.
+, -, *, /, %, ^^	Addition, subtraction, multiplication, integer division, modulo and power/exponentiation respectively.
++, --	As a postfix operator i++, increase i by 1 (resp. decrease for --). Also note the ++ binary operator above.
new T(<args>)	Creates a new object of type T.
new T[length]	Creates a new array which contains objects of type T with length number of items.
boolExpr ? exprA : exprB;	Evaluates boolExpr, if this is true it will return exprA and otherwise exprB.

Quantified Expressions

Code	Description
(\forall vars; cond; boolExpr)	Universal quantifier: For all specified variables, if they fulfil the given condition, they must fulfil the boolean expression. vars should declare one or more variables over which we will reason. For integer variables, it can also directly specify their range. cond can be any boolean expression, often used to describe the range of vars (if not already defined in vars itself). cond and the subsequent semicolon can be omitted. boolExpr is some expression that should evaluate to a boolean for all variables in the given range. Example: (\forall int i=0 .. a.length; a[i]>0), which means a[0]>0 && a[1]>0 && ... Note: the outer parentheses are required. See https://github.com/utwente-fmt/vercors/wiki/Specification-Syntax
(\forall* vars; cond; expr)	Similar construct to the \forall except that the expressions are separated by ** instead of &&. One can for example write (\forall* int j=0 .. a.length; Perm(a[j], write)) which denotes that the thread has writing access to all elements in a. Note: the outer parentheses are required. See https://github.com/utwente-fmt/vercors/wiki/Specification-Syntax
(\exists vars; cond; expr)	Evaluates to true if expr evaluates to true for at least one of the possible assignments to the variables in vars, where the assignment also satisfies the condition cond. The latter and the respective semicolon can be omitted. Note: the outer parentheses are required. See https://github.com/utwente-fmt/vercors/wiki/Specification-Syntax
array[*]	This is syntactic sugar for a \forall* expression that ranges over all elements in the array array, typically used in a Perm expression. Instead of the example above for \forall*, you can then write Perm(array[*], write). This cannot be used within nested \forall* expressions. See https://github.com/utwente-fmt/vercors/wiki/Permissions
(\forperm T1 o1, ..., Tn on \in loc; expr)	Universal quantifier over accessible locations: Boolean expression expr has to hold for all variables o1 of type T1, ..., on of type Tn for which we currently have at least read permission to loc. Example: (\forperm MyClass obj \in obj.f; obj.f==0) Note: the outer parentheses are required.

Specification-only Expressions

Code	Description
\result	The value that the method returns, only allowed in postconditions. See https://github.com/utwente-fmt/vercors/wiki/Specification-Syntax
\old(expr)	Refers to the value of expr based on the heap when the method was called. This expression is typically used in postconditions (ensures) or loop invariants, but can also occur e.g. in assert statements. Note: local variables are evaluated to their current value, not their old value. See https://github.com/utwente-fmt/vercors/wiki/Specification-Syntax
held(x)	Check whether you are holding a non-reentrant lock. x should refer to the lock invariant. See also: Queue.pvl.
commited(x)	Check whether lock x has been initialised. See https://github.com/utwente-fmt/vercors/wiki/Atomics-and-Locks
idle(t)	Returns true if thread t is idle (before calling t.fork() or after calling t.join()). Overall a thread starts as idle, if the thread is forked, it goes to a 'running' state. If join is called on a running thread, then it goes back to an 'idle' state. For examples, see https://github.com/utwente-fmt/vercors/blob/dev/examples/concepts/forkjoin/
running(t)	Returns true if thread t is running. Overall a thread can go through the following states: idle --[t.fork()]--> running --[t.join()]--> idle. For examples, see https://github.com/utwente-fmt/vercors/blob/dev/examples/concepts/forkjoin/
\polarity_dependent(onInhale, onExhale)	Evaluate this expression differently, depending on whether it is inhaled (e.g. precondition when verifying method body) or exhaled (e.g. precondition when verifying calling context). onInhale and onExhale are the two forms of this expression. Note: Use with care, can easily cause unsoundness! TODO

Resources

Code	Description
Perm(var, p)	Defines permissions for variable var. If p is 1 or write then it denotes write permission, anything between 0 and 1 or read denotes read permission. Be aware that you cannot use arithmetic when using read such as read/2 or dividing read among multiple threads! Perm(...) is of the type Resource. See https://github.com/utwente-fmt/vercors/wiki/Permissions
perm(var)	The amount of permission currently held for variable var. Do not confuse with capitalised Perm above! perm(x) is of the type frac. See TODO
PointsTo(var, p, val)	Denotes permissions p for variable var similar to Perm(). Moreover, variable var points to the value val. PointsTo() is of the type Resource. See https://github.com/utwente-fmt/vercors/wiki/Permissions
Value(var)	Defines a read-only permission on the given variable. This read-only permission cannot become a write permission and it can duplicate as often as necessary. See https://github.com/utwente-fmt/vercors/wiki/Permissions
HPerm(var, p)	History permission, related to process algebra models. See https://github.com/utwente-fmt/vercors/wiki/Process-Algebra-Models
APerm(var, p)	Action permission, related to process algebra models. See https://github.com/utwente-fmt/vercors/wiki/Process-Algebra-Models
ArrayPerm(arr, i, step, count, perm)	Denotes permission p to arr[i], arr[i+step], ..., arr[i+(count-1)*step]. Currently not supported. TODO
\array(arr, len)	Shortcut for arr != null && arr.length == len. Does not specify permissions. See https://github.com/utwente-fmt/vercors/wiki/Arrays-and-Pointers
\matrix(mat, m, n)	Indicates that mat is an m by n matrix, i.e. an array of pairwise-distinct arrays. Contains read permissions for the outer array, but no permissions for the matrix elements. See https://github.com/utwente-fmt/vercors/wiki/Arrays-and-Pointers
\pointer(x, size, p)	Indicates that x is a pointer, like an array in C. Elements x[0] to x[size-1] are not NULL and can be dereferenced. For each of them, we have permission p. See https://github.com/utwente-fmt/vercors/wiki/Arrays-and-Pointers
\pointer_index(x, idx, p)	Indicates that x is a pointer or array in C, which is not NULL. For x[idx], we have permission p (no statement about other array elements). See https://github.com/utwente-fmt/vercors/wiki/Arrays-and-Pointers
\pointer_block_length(x)	The length of the pointer block (i.e. C array) that x is part of. TODO
\pointer_block_offset(x)	The offset of x within the pointer block (i.e. C array). TODO
\pointer_length(x)	TODO

Control flow constructs (PVL)

PVL provides similar control flow constructs as other languages, e.g. loops and methods. However, there are also some unique additional control flow constructs that are explained here.

Control flow construct	Example
contract returnType methodName(paramType paramName, ...) { ... }	Method definition. contract should describe the specification of the method (see "Verification flow constructs" below). returnType should be replaced by a PVL type described as above, depending on what (if anything) the method returns. methodName should be replaced by the name of the function. paramType paramName, ... is a comma-separated list of parameters, for every parameter you should define its type and its name. It is also possible to have no parameters. The body is placed within parentheses. Example: ensures \result == a + b; int sum(int a, int b) { return a + b; }
contract returnType methodName(paramType paramName, ...);	Abstract method definition. like above, except no implementation is specified in the body, just a semicolon. **Note: Be careful, it is easy to create unsoundness with abstract methods! **
contract pure returnType methodName(paramType paramName, ...) = expr;	(Pure) function definition. Similar to a method, except no side effects are allowed, and the body is just a single expression. See https://github.com/utwente-fmt/vercors/wiki/Specification-Syntax
return expr;	Exit current method and return value of expression expr. The expression can be omitted for void methods.
if(cond) thenStmt else elseStmt	Branching control flow, depending on value of boolean expression cond. Statements thenStmt and elseStmt can be single statements, or compound statements using {...}. The else branch can be omitted.
loopContract for (init; cond; update) stmt	Classic for loop. loopContract defines loop invariants and variants as defined below. The body stmt can be a single statement, or compound using {...}. The initialisation init can be one or more statements separated by comma, or omitted. The same holds for the update statement(s). The boolean expression cond can also be omitted.
loopContract for(T var = lo .. hi) stmt	Ranged for loop. loopContract and stmt as above. The loop variable var(of type T) ranges from lo (incl.) to hi (excl.).
loopContract while (cond) stmt	Classic while loop. loopContract and stmt as above, boolean condition cond.
par identifier(iters) contract { ... }	Parallel block. See https://github.com/utwente-fmt/vercors/wiki/Parallel-Blocks
parallel { parBlocks }	TODO
sequential { parBlocks }	TODO
vec (iters) { ... }	Vector block: A variant of the parallel block where every step is executed in lock step. iters should define what variables are iterated over, e.g., int i = 0..10. Not the absence of a contract, compared to regular par blocks.
atomic(inv) { ... }	Atomic block: performs the actions within the block atomically. See https://github.com/utwente-fmt/vercors/wiki/Atomics-and-Locks
invariant invName(expr) { ... }	Define resource expression expr as a named invariant that can then be referenced inside the given block {...}, e.g. by an atomic
barrier(identifier) contract { ... }	Barrier: waits for all threads to reach this point in the program, then permissions can be redistributed amongst all threads, after which the threads are allowed to continue. See https://github.com/utwente-fmt/vercors/wiki/Parallel-Blocks
fork expr;	starts a new thread.
join expr;	waits for the specified thread to complete.
wait expr;	pause the thread until it is notified to continue.
notify expr;	notify another thread that it may continue if it is waiting.
lock expr;	Acquire a lock. See https://github.com/utwente-fmt/vercors/wiki/Atomics-and-Locks
unlock expr;	Release a lock. See https://github.com/utwente-fmt/vercors/wiki/Atomics-and-Locks
label l;	Label: indicates a location in the program that can be jumped to with goto l.
goto l;	jump to the location of the label l.
communicate x.f1 -> y.f2;	VeyMont syntax: send value of field x.f1 to field y.f2. Opposite direction also possible via <-.

Verification flow constructs

Code	Description
assert expr;	Check that boolean or resource expression expr holds at this program point.
assume expr;	Assume without checking that boolean expression expr holds at this program point. ** Note: Careful, can easily cause unsoundness! **
requires expr;	Method or function precondition: Boolean or resource expression expr is checked to hold when calling this method, and assumed to hold when verifying the method body. Defined as part of a method contract, as well as e.g. contracts for parallel blocks.
ensures expr;	Method or function postcondition: Boolean or resource expression expr is assumed to hold immediately after calling this method, and checked to hold when verifying the method body. Defined as part of a method contract, as well as e.g. contracts for parallel blocks.
context expr;	Shorthand that combines requires expr and ensures expr.
loop_invariant expr;	Loop invariant: Boolean or resource expression expr must hold before entering the loop and after each loop iteration. Part of a loop contract.
context_everywhere expr;	Shorthand that combines requires expr and ensures expr. Moreover, it also adds loop_invariant expr; to all loops within the method. Part of a method contract.
given T p;	Ghost input parameter: Defines a specification-only parameter p of type T that must be passed when this method is called (see given above). Part of a method contract.
yields T p;	Ghost output parameter: Defines a specification-only return value p of type T. p can be assigned in the method body like a local variable; the last assigned value is automatically returned to the caller, who can store it in their own local variable (see yields above). Part of a method contract.
fold pred(...);	Fold a predicate, i.e. wrap permissions inside. See https://github.com/utwente-fmt/vercors/wiki/Predicates
unfold pred(...);	Unfold predicate, i.e. unwrap the contained permissions. See https://github.com/utwente-fmt/vercors/wiki/Predicates
\unfolding pred(...) \in expr	Temporarily unfold predicate in (pure) expression expr. See https://github.com/utwente-fmt/vercors/wiki/Predicates
refute expr;	Disproves expr at this program point. Internally it is translated to assert !(expr).
inhale expr;	Take in the permissions specified in the resource expression expr, i.e. add them to the current set of permissions without checking. Additionally, assume without checking all boolean properties contained in expr. Note: Be careful, this can easily lead to unsoundness!
exhale expr;	Assert all permissions and boolean properties contained in expr, then discard the specified permissions, i.e. remove them from the current set of permissions.
witness x;	Obsolete syntax to declare witness names for the old backend Chalice. This feature is deprecated and should no longer be used.
send channelName, delta: expr;	Transfer permissions and boolean facts contained in the resource expression expr to another thread, identified via the channel name. Used within parallelised loops, and delta is the amount of loop iterations how far the expression is sent ahead. Example: send S,1: Perm(arr[i+1], 1\2); sends permission for the next array element to the next iteration. That way, the next iteration can write to its arr[i], even if it did not originally have all the permission. See e.g. https://github.com/utwente-fmt/vercors/blob/dev/examples/concepts/arrays/JavaArrayExamples.java. See also recv below.
recv channelName;	Receive the expression sent by a send as specified above, with the matching channel name. Blocks until it is received.

Histories & Futures

Histories and futures, jointly referred to as "Process algebra models" are currently under redesign. Thus, the following parts may not be up to date.

Defining processes

Code	Description
process	Type of actions and defined processes in histories.
process1 + process 2	Do either process1 or process2
process1 * process 2	Sequential composition, do process1 followed by process2
process1 || process 2	Parallel composition, do process1 and process2 at the same time (interleaved)

History-related constructs

Code	Description
History hist	Declare a History object called hist
HPerm(var, p)	History-specific permissions where var refers to a variable in the history and p is the amount of permissions (a value between 0 and 1)
APerm(var, p)	History-specific permissions within action blocks where var refers to a variable in the history and p is the amount of permissions (a value between 0 and 1)
Hist(var, p, val)	Similar to PointsTo, it denotes permissions p for variable var (which is in a history). Moreover, variable var points to the value val.
AbstractState(h, boolExpr)	This can be used to check that the given boolean expression holds in the history (or future) h
action(h, perm, preState, postState) { ... }	The action describes how the state of the history (or future) is changed by the code within { ... }. The pre- and post-state describe the state of the history (or future) in terms of processes. perm describes the permissions we have on the history (or future) and h is the name of the history (or future)
create h	Create a history. Note that the History class should be instantiated beforehand.
destroy h, val	Destroy a history h which has the value val
split h, p1, val1, p2, val2	Split a history (or future) into two such that the first part has permissions p1 and value val1 and the second part has permissions p2 and value val2
merge h, p1, val1, p2, val2	Merge two histories (or futures) such that resulting history h has permissions p1+p2 and consists of combination of the actions described in val1 and val2
modifies vars	List of locations that might be modified
accessible vars	List of locations that might be accessed

Future-related constructs

Code	Description
Future f	Declare a Future object called f
Future(f, p, val)	It denotes that we have permissions p on future f of which the state is val
choose f, p1, pre, post	//TODO check this support and definition
create f, val	Create a future f with the initial state val
destroy f	Destroy the future f