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

• 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.

• Specification-only elements 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.

• 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 (set) that does not allow duplicates. 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 (bag or multiset) that does allow duplicates. 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 (map, record or dictionary) that does not allow duplicate keys. 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 of the type None or of the type 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)) See TODO
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.
==>	Logical implication. The left side should be boolean-typed, the right side boolean or resource. Lower precedence than ||. 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 &&. See https://github.com/utwente-fmt/vercors/wiki/Permissions
-*	Magic wand or separating implication. Same precedence as ==>. 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	// unclear. Legacy syntax? TODO
then	// unclear. Legacy syntax? 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)
+	Sequence concatenation, Set union, Bag union
xs[k]	Sequence indexing: ith 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)	// unclear. Probably creating a sequence that stores the values from array e1 between indices e2 and e3. TODO
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.
{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.
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.

PVL

Code	Description
==, !=	Equals and not equals for reasoning about the equality of expressions
&&, ||, !	And, or, and negation respectively for reasoning with boolean variables.
<, <=, >, >=	Smaller than, smaller than equals, greater than and greater than equals respectively. They are used to compare integers.
+, -, *, /, %, ^^	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 col; expr)	Universal quantifier over accessible locations: expr has to hold for all variables o1 of type T1, ..., on of type Tn in collection col(? TODO), for which we currently have at least read permission. Note: the outer parentheses are required. See https://github.com/utwente-fmt/vercors/wiki/Specification-Syntax

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.
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 'runnning' state. If join is called on a running thread, then it goes back to an 'idle' state.
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

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() 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(langExpr, langExpr, langExpr, langExpr, langExpr)	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(langExpr)	TODO
\pointer_block_offset(langExpr)	TODO
\pointer_length(langExpr)	TODO
\polarity_dependent(langExpr, langExpr)	TODO

Control flow constructs

Control flow construct	Example
Function	contract returnType functionName(paramType paramName, ...) { ... }. contract should describe the specification of the method. returnType should be replaced by a specific type or void depending on what (if anything) the method returns. functionName 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. For example: ensures \result == a + b; int sum(int a, int b) { return a + b; } is a function which returns an integer that is the sum of the parameters given. Pure and Abstract Functions: Pure functions are declared by prepending modifiers static and pure in that order. They should be side-effect free and their postconditions must not contain resource assertions such as accessibility predicates. All accessibility constraints for the body of the function and for the postcondition should be ensured by the preconditions. In fact, since pure functions applications are side-effect-free, pre- and post-states of a function application are the same. Example: requires a != null; requires 0 <= n && n <= a.length; requires (\forall* int j; 0 <= j && j < a.length; Perm(a[j],1\2)); ensures (n==a.length)? \result == 0 : \result == a[n] + sumAll(a,n+1); static pure int sumAll(int []a, int n); Notice that in the example the function has no body. By doing so we declare an abstract function. When calling this function, its pre-conditions will be checked and its postconditions assumed. No correspondence should be assumed between pure and abstract functions.
Return	return can be used to exit the current method. return expr can be used within a method to return a specific object as a result.
If-statement	Single-line option: if (boolExpr) ...; Multi-line option: if (boolExpr) { ... }
If-then-else	if (boolExpr) { ... } else { ... }
For-loop	loop_invariant p; for (...) { ... }
While-loop	loop_invariant p; while (boolExpr) { ... }
Parallel block	par contract { ... } OR par identifier(iters) contract { ... }. The identifier is optional and iters can be empty. iters specifies what variables are iterated over. Note that you can also extend a parallel block with another parallel block as follows: par contract { ... } and contract { ... } OR par identifier(iters) contract { ... } and identifier(iters) contract { ... }.
Vector block	vec (iters) { ... } is a variant of the parallel block where every step is executed in lock step. You do not need to specify a pre- and postcondition. iters should define what variables are iterated over, e.g., int i = 0..10.
Atomic block	atomic(inv) { ... } performs the actions within the block atomically. As a result, other threads will not be able to see any intermediate results, only the result before or after executing the atomic block. inv refers to an invariant which stores permissions that are necessary when executing the atomic block.
Barrier	barrier(identifier) contract { } waits for all threads to reach this point in the program, then permissions can be redistributed amongst all threads, as specified in the contract, after which the threads are allowed to continue. The barrier needs to know how many threads should reach it before everyone is allowed to continue, this is done by specifying identifier which refers to a parallel block before the barrier.
Fork a thread	fork expr starts a new thread.
Join a thread	join expr waits for the specified thread to complete.
Wait	wait expr will pause the thread until it is notified to continue.
Notify	notify expr will notify another thread that it may continue if it is waiting.
Acquire a lock	lock expr
Release a lock	unlock expr
Label	label l indicates a location in the program that can be jumped to with goto l.
Goto	goto l indicates control flow must be transferred to the location of the label l.

Note that for-loops and while-loops should be preceded with a contract consisting of one or more loop invariants. Parallel blocks require a contract in the form of requires/ensures clauses.

Verification flow constructs

Code	Description
assert expr	Defines an assert statement expr which describes a condition that should hold at the program point where this statement is defined.
assume expr	Defines a statement that assumes that expr holds. It can be put anywhere within the code.
requires expr	Defines the precondition as expr, i.e., expr must hold when calling this method. The precondition should be specified before the method declaration.
ensures expr	Defines the postcondition as expr, i.e., expr must hold when completing this method. The postcondition should be specified before the method declaration.
context expr	This is an abbreviation that combines the statements requires expr and ensures expr. This statement should be specified before the method declaration.
loop_invariant expr	Defines a loop invariant expr which is a condition that must hold when entering the loop and after each loop iteration. A loop invariant should be specified before the corresponding loop.
context_everywhere expr	This is an abbreviation that combines the statement requires expr and ensures expr. Moreover, it also adds loop_invariant expr to all loops within the method. This statement should be specified before the method declaration.
given T p	Defines that a ghost input parameter (specification-only parameter) of type T with the name p is passed when this method is called. This statement should be specified before the method declaration.
yields x	Returns a ghost output parameter (specification-only parameter) to the callee of this method. This statement should be specified before the method declaration.
with ... then ...	with is used to pass a parameter to a method (which has a given statement) and then can be used to store a returned value from a yields statement. This statement is specified after the corresponding method call (on the same line) where you want to pass the parameter. All the ... should be replaced by an assignment.
unfolding ... in expr	Temporarily unfold definitions in (pure) expressions. The ... should be replaced by a predicate.
refute expr	Disproves expr at the given program point. This statement can be put anywhere in the code. Internally it is translated to assert !(expr).
inhale p	Take in the specified permissions and properties.
exhale p	Discard the specified permissions
fold x	Wrap permissions inside the definition
unfold x	Unwrap a bundle of permissions
witness x	Declares witness names. This feature is deprecated and should no longer be used.

Histories & Futures

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)
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

Other

• APerm ??
• Ls: send p to Lr, d | Release permissions p to the statement labelled Lr with d being the distance of dependence. This statement is labelled Ls.
• Lr: recv p from Ls, d | Acquire permission p from the statement labelled Ls with the distance of dependence d. This statement is labelled Lr.
• Iteration contract | An iteration contract specifies the iteration's resources. The precondition of an iteration contract specifies the resources that a particular iteration needs, and the postcondition specifies the resources that become available after the execution of the iteration.
• \pointer(var, length, perm), \pointer_index(...)?