Crowbar support asynchronous contracts (in interfaces), synchronous contracts and object invariants (in classes) and cooperative contracts (mixing both).

Object invariants are expressions that have to hold at every point a method gains control over the object, i.e., at every method start and every reactivation after an await statement. It has to be proven to hold at every method termination, every suspension at an await statement and after the initial block terminates.

Object invariants are specified with two annotations

• [Spec: ObjInv(inv)] class ... specifies that inv is an object invariant.
• [Spec: Requires(req)] class ... specifies that req is a precondition for object creation, i.e., it has to hold upon object creation.

The proof obligation of the initial block states that if req holds after creation, then inv holds after executing the initial block init.

The default specification pair is true/true.

Loop invariants are predicates that have to hold at the beginning and end of each loop iterations.#

They are annotated using [Spec: WhileInv(e)] while...

The default loop invariant is true.

Asynchronous method contracts are pre-/postcondition pairs at the interface level. The precondition describes only the parameters and the postcondition described the return value (and can use the parameters to do so). Each caller must adhere to the precondition for an asynchronous call with !, which is automatically added to the proof obligation by the system. Example:

interface I{
   [Spec: Requires(i >= j)] 
   [Spec: Ensures(result == i+j)] 
   Int add(Int i, Int j);
}

The default contract is true/true. Contracts are inherited by subinterfaces.

Synchronous method contracts are pre-/postcondition pairs at the class level. The precondition describes only the fields and the postcondition described the return value and the fields of the class. Each caller must adhere to the precondition for a synchronous call with ., which is automatically added to the proof obligation by the system. Each such caller must additionally adhere to the asynchronous contract. Contract may use old and last to refer to the prestate before method execution (old) or before the last suspension (last).

Example that states that a field counter is only increased after method execution.

[Spec: Requires(this.counter == 0)] 
[Spec: ObjInv(this.counter >= 0)] 
class C(Int counter) implements I{
   [Spec: Ensures(this.counter >= old(this.counter))] 
   Int add(Int i, Int j){ ... ]

   Int demo(){
      this.counter = 5;
      this.add(1,2);
      assert this.counter >= 5; //guaranteed to hold
   }
}

The default contract is true/true.

When asynchronously calling methods with synchronous contracts, it is not safe for the callee to assume the synchronous precondition, as it must be ensured by the last terminated process, not the caller. This can be ensured by annotating context sets to specify which methods are candidates to be the last terminated process and must ensure the precondition (of the callee) as an additional postcondition (of the last process). Then, a special step called propagation ensures that all contracts are consistent.

Crowbar does not implement propagation. Instead, it outputs static nodes that must be processed by an external static analysis to ensure consistency. Such analyses are not based on program logics.

Similarly, we allow to annotate get statements with resolving contracts. A resolving contract is a set of method names and the synchronization is allowed only on futures from these methods. Their asynchronous post-condition is used for the future. Again, Crowbar does not implement the external analysis. It is, e.g., implemented as a points-to analysis is SACO.

class D implements J{
   Int demo(Fut<Int> f){
      [Spec : Resolves("M.I.add")]
      Int i = f.get;
      assert i >= 0; //guaranteed to hold, but outputs a static node
   }
}

Requires/Ensures pairs are also allowed at function definitions.

To verify all proof obligations in a programs, run (from the root directory after building).

java -jar build/libs/crowbar.jar <path/to/files> --full

The option --full verifies all elements of the program, i.e., all classes, interfaces, functions and the main block. For more targeted verification, use one of the following options. All identifiers must be fully qualified.

• -m, --method <module>.<class>.<method> verifies a single method <module>.<class>.<method>
• -i, --init <module>.<class> verifies the initial block of <module>.<class>
• -c, --class <module>.<class> verifies the initial block and all methods of <module>.<class>
• -f, --function <module>.<function> verifies the function <module>.<function>
• --main verifies the main block of the model. If a model has several main blocks, Crowbar verifies the one chosen by the ABS compiler as the starting point.

Crowbar supports the following additional parameters.

• To generate an executable counterexample from all failed proof branches, set the flag -inv, --investigate (default: off). The generated ABS files will be written into a temporary directory, which can be set with -t, --tmp (default: /tmp/).
• To get more (or less) output from Crowbar, use the --verbose option with a value 0,1,2,3 (default: 1).
• To shorten the output SMT-LIB proves, set the flag--concise_proofs (default: off).
• To use a different system for verification, set the -d, --deduct option. Local types are selected with --deduct LocalType, the standard system is selected with --deduct PostInv (default: PostInv).
• To use a different SMT-solver, set the -s, --smt <path/to/solver> option. It will be called using <path/to/solver> <path/to/tmp>/SMT-LIB-output.smt. (default: z3).
• To use a lightweight deadlock analysis that output the methods that cannot be part of any deadlock cycle, set the flag -fr, --freedom (default: off).
• To output an overview over the available options, use -h, --help.

The following uses an alternative path to a solver to verify a single method against its local type with extra debug output.

java -jar build/libs/crowbar.jar example.abs --method Mod.Cla.Met - d LocalType -v 3 -s /bin/mysolver

Crowbar is fully automatic, it is not possible to interact with the proof system interactively.