In our new programming language, contracts can define states. For example, a LightSwitch
is always either Off
or On
(never both):
contract LightSwitch {
state On;
state Off;
}
Methods, including constructors, can change the state of this
with the ->
operator:
LightSwitch() { // constructor
->Off; // Transition to Off state.
}
Methods can specify what states the object must be in before they can be invoked and what states the object will be in after they exit by annotating the this
parameter. Constructors can specify what state they end in.
LightSwitch@Off() { // constructor always ends with the object in Off state
->Off;
}
transaction turnOn(LightSwitch@Off >> On this) // turnOn() can only be called on objects that are in Off state.
{
->On;
}
transaction turnOff(LightSwitch@On >> Off this)
{
->Off;
}
Each object can have one reference that statically specifies what state the object is in. For example, LightSwitch@On
is the type of a variable that refers to a switch that is in On
state.
transaction foo() {
LightSwitch s = new LightSwitch();
s.turnOn();
}
The compiler checks transaction invocations to make sure they are safe:
transaction foo() {
LightSwitch s = new LightSwitch();
s.turnOff(); // COMPILE ERROR: turnOff() requires that s is On, but here s is Off
}
As before, the programmer can use []
statements to check state information at compile time. For example, [s@Off];
will cause a compiler error if s
does not refer to an object in Off
state.
Unowned
. For example:
transaction foo(LightSwitch@Unowned s) {
s.turnOff(); // COMPILE ERROR: can't change state of s through an unowned reference
}
Shared
. These references can be used to change the state of the referenced object, but invoking transactions that can only be called in some states requires a runtime check. For example:
transaction test1(LightSwitch@Shared s) {
s.turnOn(); // COMPILE ERROR: turnOn requires that s be Off, but s is Shared.
}
In the above situation, the programmer might need to check the state dynamically with if...in
.
is
transaction test2(LightSwitch@Shared s) {
if (s in On) { // runtime check to see whether the object referenced by s is in state On
s.turnOff(); // OK due to runtime check
}
}
Within the scope of the if...in
block, the compiler requires that if there s
, then the owner's state specification is never violated. If it is, then the program is terminated; it is up to the programmer to make sure the body of the if is
block does not change the state inappropriately.
When a Shared
reference is needed, an Owned
suffices as long as the reference is NOT to an asset. For example, an Owned
reference can be passed as an argument to a transaction that expects a Shared
reference to a non-resource object. However, the caller is left with a Shared
reference.
When an Unowned
reference is needed, any reference suffices, and the caller is left with their original kind of reference.