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.
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.
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
- 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
- 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.
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:thesis).
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.