Properties of Routines
- Routines have no side-effects.
- Routines always terminate.
- Routines can only invoke other routines.
Code in Stella can be either imperative or reactive. Both kinds of code can operate on the same data, but the allowed sets of operations differ. Whereas imperative code may use the full power of a Turing-complete language, reactive code is restricted to operations that are guaranteed to terminate and that are free from side-effects. To uphold these constraints, abstract data types in Stella are represented by classes which may define local fields, constructors, methods, as well as routines. Routines are special kinds of methods whose expressive power is a strict subset of that of methods.
Routines that contain expressions with side-effects
(set! and a couple of other special forms) are rejected by the interpreter.
A run-time error occurs when a routine calls a method, for example println!
which performs IO.
Stella uses Size-Change Termination for higher-order programs to ensure at run-time that routines terminate. We implemented the algorithm described in the following paper, and slightly adapted it to fit our object-oriented model.
Phúc C. Nguyễn, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn. 2019. Size-change termination as a contract: dynamically and statically enforcing termination for higher-order programs. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2019). Association for Computing Machinery, New York, NY, USA, 845–859. DOI: https://doi.org/10.1145/3314221.3314643
The Pair class can be used to represent linked lists.
It shows how classes are defined, and we use it to demonstrate the guaranteed termination of
routines.
Local fields are declared via def-fields.
A constructor is defined called initialize-with
with 2 formal parameters called initial-car and
initial-cdr that will initialize the fields of a new pair.
Routines are defined via def-routine, such as the routines called
first and second with no arguments which are "getters" for the
car and cdr field.
Two methods are defined called set-first! and set-second! which are
setters for these fields.
Finally, a routine length is defined that will compute the length of a
linked list by calling length on the cdr field as long
as it is also a pair.
Running this program demonstrates that a call to length will be rejected.
In the definition of the Main actor behaviour, an instance of Pair
is created (and stored in variable p1),
and via a call to its set-second! method it is made to point to itself.
A subsequent call to its length method of the pair is successfully rejected
by the interpreter. This call would otherwise result in an infinite loop.
Try it out! Remove the method invocation
(length p1), either by removing the line of code entirely, or by adding
// at the front (commenting out the line), and re-run the program.
Now that the offending invocation is gone, the program no longer throws an error.