A consideration was made, whether communication of null values instead of objects should be allowed.
While sending null values could be considered a violation of protocol, it is an important aspect of the Java language that any object may be null.

It was decided to follow Scribble-Java's lead, after some testing it was revealed that Scribble-Java does allow null values to be communicated instead of objects.

Currently, even when the unsupported language features are removed. Unexpected errors still occur.
Simplifying Adder.java and Adder_C_1.java of the Scribble Adder example until it succesfully verifies leads to the following code:

Adder,java:

package tutorial.adder.Adder.Adder;

public final class Adder {
	public static int state;
}

Adder_C_1.java:

package tutorial.adder.Adder.Adder.statechans.C;

import tutorial.adder.Adder.Adder.Adder;

public class Adder_C_1 {

	//@ context Perm(Adder.state, 1);
	//@ ensures Adder.state == 1;
	public Adder_C_1() {
		Adder.state = 1;
	}

	//@ context Perm(Adder.state, 1);
	//@ requires Adder.state == 1;
	//@ ensures Adder.state == 2;
	public void send(int arg0, int arg1) {
		Adder.state = 2;
	}

	//@ context Perm(Adder.state, 1);
	//@ requires Adder.state == 1;
	//@ ensures Adder.state == -1;
	public void send() {
		Adder.state = -1;
	}
}

It does give off warnings:

If attribute state has a default variable as such: public static int state = 0; VerCors gives the following error:

If send has Integer parameters as opposed to int then VerCors gives an error as well.

Currently state objects being returned are not verified not to return null.
They cannot return null, however we should verify this, so that method calls on these objects can be verified as well.

See utwente-fmt/vercors#739 for a more detailed explanation of this issue.

Currently Scribble-Java creates a class for each state, named as such: protocol_role_number (for example: Adder_C_1).
These classes contain the methods enabled at these states, this statically guarantees that for a state only the enabled methods are used.
However it is up to the user to use the correct state.

We propose to use only the methods so the generated code more closely resembles the actual Scribble protocol.
VerCors will verify that only enabled methods are used.

We have already shown that VerCors can verify state for the current implementation where methods are part of the state class.
In cases where the same method is used in multiple states we should be able to verify this as follows:

Imagine the Adder example except there need to always be an even number of additions, so we need to do Add and Res twice before we can stop:

global protocol Adder(role C, role S) {
	choice at C {
		Add(Int, Int) from C to S;
		Res(Int) from S to C;
		Add(Int, Int) from C to S;
		Res(Int) from S to C;
		do Adder(C, S);
	} or {
		Bye() from C to S;
	}
}

Now we have a method Add that can be executed from multiple states, we can verify that it is executed correctly as follows:

//@ context Perm(state, 1);
//@ requires state == 1 || state == 3;
//@ ensures (\old(state) == 1 && state == 2) || (\old(state) == 3 && state == 4);
public void add(int p1, int p2) {
  if (state == 1)
    state = 2;
  else if (state == 3)
    state = 4;
}

Connection between roles has not yet been implemented.
A Scribble protocol can be either implicit or explicit.
In both cases, user input will be needed to provide locations (IP/port) of the other roles.

In the case of an explicit protocol, roles have to connect and disconnect to each other in the protocol.
These connections are bi-directional and must be distinct.
I need to investigate how Scribble-Java handles them.

In the case of an implicit protocol: the protocol starts with all roles pairwise connected.
However in Scribble-Java making the connections is left to the user (and is susceptible to deadlocks).
In their Adder example C connects to S in the user code, if S is not started before C the connection fails.

Info on Scribble connections taken from: http://www.scribble.org/docs/scribble-java.html#SCRIBCONNECT

1. TypeArgumentsOrDiamond such as new LinkedList<>() or new LinkedList<String>()
2. JavaIdentifier such as org.scribble.core.type.name.GProtoName as opposed to GProtoName
3. Annotation such as @Override

Generated Scribble code of the Adder example generates code that throws custom exceptions of type ScribRuntimeException.
I do not know what this exception is meant to represent as it just extends Exception and the only documentation states that it is actually not a Scribble run-time exception: "Note: not a run-time ScribbleException".

Problem:
The verification skeleton cannot have these exceptions however, as exceptions must extend Throwable and VerCors does not support inheritance.
Default Java exceptions (IOException) are fine however, implying that VerCors treats default Java classes differently.

Removing these exceptions only from the verification skeleton is not an option as user code will still need to handle them.
This means that it is impossible to verify generated code + user code without changing the generated code, even if using the verification skeleton.

External choice is not modeled by the automaton and as such is treated like an internal choice.
A choice must be received from the other party and operations may only be executed if they have been chosen.
A choice may only be received if it is made according to the protocol.

To represent the different choices:
Enums are not allowed by VerCors and static constants cannot be used either as assigning a value in a declaration gives an error in Vercors as well.
To solve this, constant attributes can be given a value in the constructor. While a variable holds the current choice.

External choice can be handled as such by generated code:

package adderpkg;


public class Adder
{
	int state;
	int choice;
	public final int EXTERNAL_CHOICE_ADD;
	public final int EXTERNAL_CHOICE_BYE;

	//@ ensures Perm(state, 1) ** Perm(choice, 1) ** Perm(EXTERNAL_CHOICE_ADD, 1) ** Perm(EXTERNAL_CHOICE_BYE, 1);
	//@ ensures state == 14 && choice == -1 && EXTERNAL_CHOICE_ADD == 0 && EXTERNAL_CHOICE_BYE == 1;
	public Adder() {
		choice = -1;
		state = 14;
		EXTERNAL_CHOICE_ADD = 0;
		EXTERNAL_CHOICE_BYE = 1;
	}

	//@ context Perm(state, 1) ** Perm(choice, 1);
	//@ context state == 14;
	//@ requires choice == -1;
	//@ ensures (\result == 0 || \result == 1) && \result == choice;
	 public int receiveExternalChoice() {
		choice = 0;
	 	return 0;
	 }
	
	//@ context Perm(state, 1) ** Perm(choice, 1);
	//@ requires state == 14 && choice == 0;
	//@ ensures state == 16 && choice == -1 && \result != null;
	public AddPayload add()
	{
		choice = -1;
		state = 16;
		return new AddPayload(0, 0);
	}
	
	//@ context Perm(state, 1) ** Perm(choice, 1);
	//@ requires state == 14 && choice == 1;
	//@ ensures state == 15 && choice == -1;
	public void bye()
	{
		choice = -1;
		state = 15;
	}
	
	//@ context Perm(state, 1);
	//@ requires state == 16;
	//@ ensures state == 14;
	public void res(int arg0)
	{
		state = 14;
	}

	public static void test() {
		Adder adder = new Adder();
		if (adder.receiveExternalChoice() == adder.EXTERNAL_CHOICE_ADD) {
			adder.add();
			adder.res(0);
		}
		else
			adder.bye();
	}
}