# Contracts and Invariants

The following code verifies that Euclid's algorithm returns a positive number if run on positives input. To try it out, run Crowbar on `examples/gcd.abs`.

``````module CallS;

interface GcdI {
[Spec : Requires(p1 >= 0)] [Spec : Requires(p2 >= 0)]
[Spec : Ensures(result >= 0)]
Int gcd(Int p1, Int p2);
}

interface LogI {
[Spec : Requires(p1 > 0)] [Spec : Ensures(result > 0)]
Int log(Int p1);
}

[Spec : Requires(log != null)] [Spec : ObjInv(log != null)]
class GcdC(LogI log) implements GcdI{
Int gcd(Int p1, Int p2){
Int a = p1;
Int b = p2;
Int ret = 0;

if (a == 0){ ret = b; }
else {
[Spec: WhileInv(b >= 0 && a > 0 && log != null)]
while(b != 0){
if( a > b ) a = a-b;
else        b = b-a;
}
log!log(a);
ret = a;
}
return ret;
}
}

[Spec : Requires(this.f == 0)] [Spec : ObjInv(this.f >= 0)]
class LogC(Int f) implements LogI{
[Spec: Ensures(result == this.f)]
Int log(Int p1){
this.f = this.f + p1;
return this.f;
}
}

{
LogI log = new LogC(0);
GcdI gcd  = new GcdC(log);
Fut<Int> f = gcd!gcd(10,5);
}
``````

The method `GcdI.gcd` is specified interface in the as taking two positive numbers (`[Spec : Requires(p1 >= 0)] [Spec : Requires(p2 >= 0)]`) and returning a positive number (`[Spec : Ensures(result >= 0)]`). Two things are worth noting here: (1) There are two preconditions, which could have been written as one precondition with a conjunction. (2) The special variable `result` is used to refer to the return value.

The method `LogI.log` is analogously specified.

The class `GcdC` is specified using a creation condition and an invariant stating that the field `this.log` is non-null (`[Spec : Requires(log != null)] [Spec : ObjInv(log != null)]`). Its methods do not need more specification than given by the implemented interface, but the loop invariant is specified using `[Spec: WhileInv(b >= 0 && a > 0 && log != null)]`.

The class `LogC` is specified using a creation condition that the counter `this.f` is initially `0` and an object invariant that is stays positive. The method `LogI.log` has a post-condition stating that the return value must be the current value of `this.f`. This is additional to the contract in the interface.

# Local Types

Crowbar also supports a lightweight version of the Session Type System for ABS. It does not perform projection, but returns a static node to notify the user that it depends on correct projection. To try it out, run Crowbar on `examples/local.abs`.

``````module Test;

[Spec:Role("server", this.s)]
[Spec:Role("client", this.c)]
[Spec:Role("database", this.d)]
[Spec:ObjInv(this.s != null && this.c != null && this.d != null)]
class C(Server s, Client c, Database d) {
// Role field aliasing
[Spec:Local("database!reset(true).Put(true)")]
Unit roleFieldAliasing() {
Database localdb = this.d;
Int a = 10;
if(a > 5) {
a = 0;
}
else {
a = 7;
}
this.d = null;
Fut<Int> sth = localdb!reset();
this.d = localdb;
}
}
``````

The specification of the class `C` uses three roles (`server`, `client`, `database`) used in the specification and connects them to fields which must contain the objects for these roles (`[Spec:Role("server", this.s)]...`). It, furthermore specifies an object invariant that these fields remain non-null. The method `C.roleFieldAliasing` is specified as calling `reset` on the `database` and then terminating (`[Spec:Local("database!reset(true).Put(true)")]`).

Note that (1) no other communication may happen, (2) that one can use additional condition and parameters and return values in the local type (`true` is used for both options here), and (3) the object playing the role of the `database` is loaded from the field containing it into a local variable and used. The system tracks the correct object and ensures that on termination and suspension the correct objects are stored in the fields assigned to roles.

# Functions

Crowbar has experimental support for pre/post-conditions for the lightweight functional layer of ABS. ADTs are fully supported. Note that termination is not checked.

``````module M;

[Spec : Requires(n > 0)]
[Spec : Ensures(result > 0)]
def Int fac(Int n) = if(n == 1) then 1 else n*fac(n-1);

{}
``````

# Counterexample Generation

To help with proof debugging, Crowbar can attempt to generate counterexamples for failing proofs using the `--investigate` flag. To see it in action, run Crowbar on `examples/ceg.abs` and see how the generated counterexample files (`/tmp/crowbar-ce-{1-5}.abs`) showcase the three issues annotated in the source code.
Or just see the abridged example below:

``````module CEG;

interface Sensor {
}

Int maxTemp = 0;

[Spec: Requires(s != null)]
[Spec: Ensures(this.maxTemp >= old(this.maxTemp))]

// Issue: this.maxTemp could be overwritten while suspended
if(temp > this.maxTemp) {
this.maxTemp = temp;
}
}
}
``````

A counterexample for the snippet above showing a case in which the value of `maxTemp` decreases in violation of the specification looks like this:

``````module Counterexample;
interface Ce { Unit ce(); }

class CeFrame implements Ce {
Int maxTemp = 1;

Unit ce() {
// Assume the following pre-state:
String s = "object_?(1)";
// End of setup

// Assume the following assignments while blocked:
this.maxTemp = -1;
// End assignments

Int temp = 0;
if((temp > this.maxTemp)){
this.maxTemp = temp;
}
// return unit
// Proof failed here. Trying to show:
// Method postcondition: (heap.maxTemp>=old.maxTemp)
// Object invariant: true
// Failed to show the following sub-obligations:
// (select(store(heap, this.maxTemp, valueOf(fut_2)), this.maxTemp)>=heap.maxTemp)
}
}
``````

We investigate the counterexample now. Context is removed, only a single class `CE` remains, which contains a single method `ce` and all fields of the original class (here: `Reader`).

The first part of `ce` sets up the required starting state (`*1`). Note that objects and futures are replaced by strings, as all external calls are abstracted by contracts and we can only compare object identity.

Then for each statement in the execution path the statement without context is added: as discussed, objects and futures accesses are replaced by Strings. `await` and calls are replaced by a re-initialization to the state after reactivation (`*2`). The original statement is added as a comment. In case of branchings, the branching itself is preserved, but the non-taken branch is removed.

Finally, at the statement that fails the proof (here: `return`), additional information about the proof obligation is given (`*3`): what properties were supposed to be shown and which property is the one that fails.

The counter-example is fully executable and can be debugged using additional output, or the debugging tools available for ABS. Here, the post-condition cannot be shown, while the (trivial) object invariant holds.