# specification language

JFSL (JForge Specification Language) is a formal lightweight specification language for Java which supports first-order relational logic with transitive closure. It provides relational and set algebra, as well as common Java operators. It also supports specification fields which can be particularly useful for specifying abstract data types.

JFSL specifications are written as Java annotations. The most commonly used annotations are:

`@Invariant("<expr>")`- defines a class invariant`@Requires("<expr>")`- defines a method precondition`@Ensures("<expr>")`- defines a method postcondition`@Modifies("f [s][u]")`- defines a frame condition for a method`@SpecField("<fld_decl> | <abs_func>")`- defines a specification field

The semantics and the syntax of JFSL expressions are
fully
explained here
(Chapter 3). It is important to know that everything is a
relation in JFSL. Classes are represented as unary
relations, whereas Java fields are represented as binary
relations (where the domain is the declaring class and the
range is the field type). The dot operator (`.`)
is actually a plain relational join, and not the field
dereferencing operator as in Java. However, because of
the inherent relational nature of object oriented
programs, in most cases the relational join operator
behaves exactly the same as field dereferencing. For
example, let `node` be a variable of
type `Node`, and let `key` be an integer
field in class `Node`. In JFSL, `node` is
represented as a singleton unary relation (a relation
containing one atom), and a binary relation (of
type `Node -> Integer`) is used to represent the
field `key`. Joining these two relations evaluates
to a singleton unary relation, containing the value of
the `key` field of the `node` instance.

# global options

There are several global options that the user may want to set before running Squander. They are listed in class GlobalOptions. Here are a couple of important remarks:

**log_level**- by default set to`NONE`, so you won't see too much information about the execution. By setting this parameter to`DEBUG`, Squander will produce verbose output, saying exactly what bounds and what formula are given to Kodkod for solving.**engine**- by default set to`Kodkod`, which should be suitable for most cases;`Kodkod2`is experimental and probably shouldn't be used;`Forge`uses Forge as the back-end, and it typically performs worse than`Kodkod`;`KodkodPart`and`KodkodPart2`both implement the KodkodPart algorithm (explained here). Differences between them are technical, and in practise`KodkodPart2`should always be a better choice.**sat_solver**- defaults to`SAT4J`which is a pure Java solver. Setting this parameter to`MiniSat`usually results in better performance, but it also requires native libraries.**unsat_core**- whether or not the solver should compute the unsat core in case when a solution cannot be found. Setting this option to`true`helps debugging your specifications but typically degrades solving performance.- other parameters don't need to be changed for most of the cases.

# @Options annotation

The `@Options`
annotation lets you specify certain options at the method
specification level. Currently, there are only a few
options available through this annotation:

**bitwidth**- allows the user to explicitly tell Squander what bitwidth to use to represent integers. Specifying this manually is rarely needed, since Squander automatically computes the minimal bitwidth necessary to represent the content of the heap. If an integer greater than the maximal integer on the heap is expected to be used (e.g. returned by the method), than it is necessary to manually set the bitwidth to a constant value.**ensureAllInts**- whether all integers (within the bitwidth) should be used, or only those found on the heap. Squander actually has a heuristic to arrive at the set of integers to be used:- if any arithmetic operation is used, all ints are used
- all integers found on the heap are added to the set of used integers, as well as array lengths, collection sizes etc.
- all integer literals found in the specifications are added to the set of used integers
- when the set cardinality operator (
`#`) is seen in the spec, all integers from 0 to max size of the relation under the "#" operator are added to the set of used integers

`ensureAllInts`option overrides this heuristic.**solve_all**- whether the solver should be capable of enumerating all solutions. This feature is still experimental. Please contact the author if you want to use it.

# java collections

Squander lets you write specifications that talk about third party classes, i.e. classes for which you don't have the source code so you can't manually annotate them with specs. Out of the box, Squander supports:

If you click on the links above, you can see the specification fields that are provided for each of those classes. Support for other third party classes can easily be implemented (more details in Chapter 6 of this thesis).# troubleshooting

JFSL type checker will catch most of the spelling and type errors in your specifications. The most common type of problems is when Squander finds no solution and you know that there should be one. In other words, you made a mistake in your specification. In some cases, the error is in the logic of your specification, i.e. the post-condition or some of the invariants are logically incorrect. A more subtle category of errors is when your logic is correct, but still you are getting no solution, due to some "technical" details. If you believe that your logic is correct, check the following:

**frame condition**- did you list all fields that must be modifiable in order to satisfy the spec? For example, if your return type is an array, then you must explicitly say that the content of that array is modifiable, i.e.`@Modifies("return.elems, return.length")`(it is similar if the return type is a Java collection class).**integers**- is the bitwidth large enough to represent all integers you care about? do you need to explicitly "ensureAllInts"? If you set the log level to`DEBUG`you'll see exactly what bitwidth and what integers are used in the final formula.**reachable portion of the heap**- set the log level to`DEBUG`to see whether all heap objects you care about are added to the Kodkod bounds. Squander could simply encode the entire portion of the heap that is reachable by following**all**fields. Instead, Squander tries to optimize the encoding and use only those fields that are mentioned/used in the spec that is being executed. So, if you realize that some objects were skipped during the translation, simply and an invariant saying that the field that leads to those objects is not null - this invariant is trivially satisfiable, it typically won't impose any performance overhead, but will help Squander discover all relevant objects on the heap.- for all other problems, please send an email to Aleksandar Milicevic.