Proposed protocol notation changes for Version 2 Milestone 2
Following a meeting with Kohei, Aybek and Tzu-Chun, we are proposing to make the following changes to the protocol notation for version 2.0.0.M2 of the scribble tools:
1) Import statement
"import" <typesystem> "<typeName>" "as" <alias> ( "," <typeName> as <alias> )* "from" "<location>" ";"
So for example, with Java it would be:
import java "Order" as Order from "org.example.data";
where "Order" is the class name and "org.example.data" is the package (i.e. the location).
For XML, this could be:
import xml "{http://www.example.org/data}Order" as Order from "../schema/Example.xsd";
2) Choice
The current choice notation has a problem in that it uses { } curly braces for the overall choice, as well as for each choice path. Through working on various examples, it is felt that the following notation is simpler:
choice from Buyer to Seller {
Order:
...
op(Cancel):
...
}
3) Recursion
With the use of <label>: for the choice paths, it was felt necessary (to avoid parser conflicts and confusion) to change the way recursion labels are defined. So for clarity, it has been made more explicit:
rec Txn {
Txn;
}
The way in which the recursion is referenced has also been changed, to remove the previously used '#' prefix.
4) Running a protocol
The way in which parameters (roles initially) are passed (or bound) when running a protocol has been changed. Instead of binding to roles defined within the protocol being run, the roles (and in future other state) are defined as parameters of the protocol. For example,
protocol BuyerSeller(role Buyer, role Seller)
The way in which the protocol parameters are passed can be in two ways:
run BuyerSeller(BuyerRole, SellerRole); -- so positional parameters
run BuyerSeller(Seller=SellerRole, Buyer=BuyerRole); -- keyword parameter assignment, as used in the current version
5) Unordered
This is a new construct:
unordered {
I1;
I2;
}
where each statement in the unordered statement can be performed in any order.
6) Try/Catch:
There are no changes to the syntax for the Try/Catch construct. However while we better understand the implications and semantics of this construct, there will be some constraints placed on what can be specified. These will be policed with validation rules.
Initially the constraints will be:
a) Catch interactions must be between same two parties and in the same direction
b) Try block must end with an interaction between the same two parties specified in the catch blocks, and in the same direction, as a way to signify that the 'try' has completed successfullly and that the 'catch' blocks will no longer be triggered.
If you have any comments on these changes, please let us know.
