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 can be verified like Java or C, 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

• Identifiers can consist of the characters a-z, A-Z, 0-9 and _. However, they must start with a letter (a-z, A-Z). 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.
• 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.
• 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 ;.

Types and Data Structures

Type	Description
int	Integer
boolean	true or false
void	Used when a method does not return anything
resource	Boolean-like type that also allows reasoning about permissions
frac	Fraction
zfrac	Fraction that can also be zero.
process	Type of actions and defined processes in histories. For more information on histories & futures, have a look at the section on Histories & Futures.
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[].
seq<T> var	Defines an immutable ordered list (sequence) named var. T should be replaced by a type.
set<T> var	Defines an immutable orderless collection (set) that does not allow duplicates. T should be replaced by a type.
bag<T> var	Defines an immutable orderless collection (bag) that does allow duplicates. T should be replaced by a type.
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.

For more information on sequences, sets, bags and options, have a look at the wiki page on Axiomatic Data Types.

Expressions

Infix Operators

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 and fractional division respectively.
++, --	Increase by 1 and decrease by 1 respectively. Unlike the other operators, this only requires an variable on the left-hand side.
==>	Implication. This statement evaluates to true unless the statement before the arrow evaluates to true and the statement after the arrow evaluates to false.
**	Separating conjunction. a ** b denotes that a and bpoint to different variables on the heap and that both expressions mus tevaluate to true. This is used to reason about multiple resources.
-*	Magic wand or separating implication. This is used to reason about resources. //TODO: investigate what is supported.
new T()	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.
(\let T t = exprA; exprB)	Evaluates exprB, replacing every occurence of t with the result of evaluatingexprA. The surrounding parens ( ) are required.

Quantified Expressions

Code	Description
(\forall vars; range; boolExpr)	Construct that allows you to repeat a certain expression for several variables. For example, (\forall int j; j >= 0 && j < n; array[j] >= 0) denotes that all elements in array nonnegative. It is equal to the following statement: array[0] >= 0 && array[1] >= 0 && ... && array[n-1] >= 0. vars should declare the variables over which we will reason. range can be any boolean expression, often used to describe the range of vars. boolExpr is some expression that should evaluate to a boolean for all variables in the given range.
(\forall* vars; range; expr)	Similar construct to the \forall except that the expressions are separated by ** instead of &&. One can for example write (\forall* int j; j >= 0 && j < array.length; Perm(array[j], write) which denotes that the thread has writing access to all elements in array.
(\exists Type id; range; expr)	Evaluates to true if there exists an element, called id, such that the final expression evaluates to true.
array[*]	This is a simplified \forall* expression that ranges over all elements in the array array. Instead of the example mentioned above for \forall*, you can then write Perm(array[*], write). This cannot be used within nested \forall* expressions.

Specification-only Expressions

Code	Description
\result	Keyword that refers to the object that the method returns
\old(expr)	Refers to the value of the specified expression in the pre-state. This can be used in a postcondition (ensures) or loop invariant in which case the pre-state is when the method was called.
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.
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.
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.

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(...)?