|
Investigating Reflective Semantics |
|
Extended Virtual Platform (XVP) |
|
The Science Building at the University of Southern Maine |
|
XVP Home |
|
The core idea of this project is that virtual platforms for languages equipped with logic-based assertions along with parametric polymorphism require proper support for these high-level language features. The main components of this architecture are a representation of logic-based constraints in class file and class object structures, a compiler that inserts these representations into a class file as additional attributes, a loader that performs appropriate actions on constraints, and reflective capabilities that report information on their associated assertions. A particularly distinctive component of this architecture, which is still under development, is an interface with a program verification system which performs checking of constraints and verifies behavioral subtyping requirements. This will be accomplished by interfacing the program verification system with reflective capabilities and performing verification by accessing type signatures and their associated constraints in class objects. The extended virtual platform is being implemented by extending the Java Virtual Machine with the proposed functionalities. Reflective capabilities that report assertions in a declarative language such as the Java Modeling Language (JML) along with runtime type information are investigated in this project. The annotated assertions are processed by the XVP compiler to generate the class file representation. However, in addition to the procedural representation of assertions that are enforced at run-time as in JML, their declarative representation is also integrated into the class file representation. The declarative representation along with the type information is loaded by the extended class loader into class objects and reported by the extended Java Core Reflection API. Some Related papers are: · Next Generation of Virtual Platforms · Temporal Verification Theories for Java-Like Classes
The developed framework currently allows the following: 1. Compilation of JML annotated features. 2. Runtime access to assertions (specifications) which allow programs to make decisions that depend upon the semantic properties of objects as specified by their associated assertions. 3. Reflection on assertions in the absence of source files. 4. Extensions of multiple types of constraint languages.
Other benefits of the proposed framework include: 1. Tools utilizing assertions could more easily be developed. 2. Data integrity of persistent systems could be maintained as explained in Next Generation of Virtual Platforms. |
|
Department of Computer Science University of Southern Maine 96 Falmouth St. Portland, Maine 04104-9300 |
|
To contact us: |
|
Phone: (207) 780-4499 E-mail: {alagic, mroyer, ddillon}@cs.usm.maine.edu |
