yak prototype

This prototype is a programming system (that includes a minimalistic programming language, type system and run-time) created to experiment the impact of adding behavioral types to an object-oriented language as well as test their usefulness in the creation and use of Web Service. This project focus on defining typing rules to statically enforce the correct use of an object's behavior (defined by a protocol) and implementing them by using deterministic finite automatons on a proof-of-concept prototype.

A more detailed description... This is an on-going project and for now the most important aspect of this prototype is the behavioral type system which checks the correct use of an object's behavior. This behavior is related to the valid sequence of method calls specified in a class' usage protocol. The protocol is a regular expression like description which tells the type system which methods can be called and in what context. Our typing rules cover all normal sequential programming constructions (if-else, while), exceptions (try-catch/throw) as well as guarantee the termination of a protocol.
A more complete presentation and additional examples (with more interesting constructions) are given in [1], therefore the following examples are only intended as a short and simple introduction to some of the prototype's features.

1. Simple example In this very simple example the usage of the Travel class follows a simple sequential order. Therefore its use reaches a valid stop position at the end the main method.

//empty and simple Travel class class Travel{ usage flight;hotel;order flight(){} hotel(){} order(){} } //Main.main (program's entry point) class Main{ main(){ Travel t = new Travel(); // Travel#flight;hotel;order t.flight(); // Travel#hotel;order t.hotel(); // Travel#order t.order(); // Travel#stop } }

2. If-Else This construction causes a branch by spliting the program flow in two different slices which are then merged back to obtain the correct shared behavior at its end.

method(A#a;((b;c)+(d;c*)) a){ if( a.a() ){ // A#((b;c)+(d;c*)) a.b(); // A#c } else{ a.d(); // A#c* }; // A#c a.c(); // A#stop a.c(); Error: illegal call }

3. While This cycle requires special attention on all possible behaviors that can occur at run-time.

method(A#a*+b v){ while( /* random */ ){ v.a(); }; // A#a* v.b(); Error: illegal call v.a(); // OK }

4. Exceptions Exceptions may cause a jump from an undetermined throw point to the appropriate catch branch based on the type of the raised object.

method(A#a[Error: b];aa v){ try{ // A#a[Error: b];aa v.a(); // possible thrown exception of type Error // A#aa }catch(Error error){ // A#b v.b(); // A#stop return; }; // A#aa v.aa(); // A#stop }

See the documentation provided in [1] for a more formal and detailed information on how each rule is checked as well as other features like subtyping, protocol recursion, assignment rules, class consistency check, behavioral argument passing.