Rewriting Logic Semantics of Beta
The Beta language is an object-oriented language with core OO features such as encapsulation, polymorphism, and inheritance. It differs from languages such as Java and Smalltalk, though, in two fundamental ways:
- Instead of different abstraction mechanisms, such as classes and methods, there is one abstraction mechanism: the pattern. Patterns can be used to create objects, run method code, handle coroutines and multiple threads, and create new control constructs.
- Instead of super calls, Beta includes an inner call. Method invocation in Beta happens "backwards" from languages such as Java -- instead of starting with the invoked method, and using super to call code implemented by a parent class, the first method invoked is the one at the top of the inheritance hierarchy (the code in Object), which then works its way back down toward the level of the caller with each inner call. This treats inheritance and method overriding as an extension of existing code with additional features, versus as a direct override of existing features with an option to call old functionality. This helps to enforce behavioral subtyping.
For more information on Beta, you can go to the Beta language home page. From there you can download the Mjolner system, the official language system for Beta. Note that there are some differences between our syntax and the syntax of Mjolner. For instance, to create a new thread in both the official Beta book (Object-Oriented Programming in the BETA Programming Language, available here) and in our version, you say something like A.fork. In the Mjolner system, you say A->fork. We also have added some syntax to make parsing easier for Maude, like putting altern(X) for a call to X that will be alternating. A full list of these changes will be available here soon.
Our current release is version 0.91. We are missing several features in the language that will move us to version 1.0, including:
- inner calls given an explicit name (we have inner, not inner P)
- nondeterministic alternation
- support for suspend on concurrent threads
The files are available here. These include the basic files, some samples, and an experimental extension of Beta with super calls (inspired by Goldberg, Findler, and Flatt's OOPSLA 2004 paper). Note you will need Maude to run these. To run the examples, you can just load the examples file -- it will load everything it needs. The semantics will pull in the syntax automatically.
NOTE: We have removed the files while we fix two problems that were pointed out to us with the semantics. An explanation of the problems, as well as details of the fixes, will be available soon.
- all the files in the current distribution: beta.tar.gz
- Beta syntax: beta-syntax.maude
- Beta semantics: beta-semantics.maude
- example programs: beta-examples.maude
- Beta model checker: beta-modelcheck.maude
- Beta syntax with super methods: beta-syntax-wsuper.maude
- Beta semantics with super methods: beta-semantics-wsuper.maude
- A simple example using super: beta-super-example.maude
These files were updated from version 0.9 on Nov 15, 2005. Two main changes were made. The first change was a fix in assignment to remote names (such as 5 -> a.b). Assignment should now work in all cases. The second change was to the comments, not to the definition. For some of the todo comments, the changes were made before the 0.9 release but the todo was never removed. These comments have now been removed to avoid causing confusion (by, for instance, indicating a working feature still needs to be defined).
- An Executable Semantic Definition of the Beta Language using Rewriting Logic
- Mark Hills, T. Baris Aktemur and Grigore Rosu
Technical Report UIUCDCS-R-2005-2650, November 2005
PDF, TR@UIUC, BIB