B.  Programming Language

In this appendix, we sketch the language that is used in the RISC ProgramExplorer for describing programs (its formal syntax is described in Appendix H.1). This programming language can in the following sense be considered as a “MiniJava”, i.e. as (a variant of) a subset of Java: Assume that a program can be parsed and type-checked by the RISC ProgramExplorer without error. If this program can be also compiled by the Java compiler without error, then the execution of the generated target code behaves as specified by Java¹ .

Deviations In detail, MiniJava has the following deviations compared to Java (such that a program that can be parsed and type-checked by the RISC ProgramExplorer cannot be compiled in Java):

Visibility Modifiers

The modifiers public, protected, and private are recognized but ignored; in fact MiniJava treats all entities as if declared with modifier public. Consequently, if a MiniJava program violates the specified access constraints, it cannot be compiled by a Java compiler.

Constraints The following items describe constraints of MiniJava (such that a program that can be compiled with Java cannot be parsed or type-checked by the RISC ProgramExplorer)² .

Inheritance

MiniJava does not support inheritance; every class denotes an object type that is incompatible with the object type of any other class.

Interfaces

MiniJava does not support interfaces.

Method Calls

A method call with a return value may only appear on the right side of of a variable initialization or of a variable assignment, not as an expression within another expression.

For Loops

The initialization part of a for loop header must be an initialized variable declaration or a variable assignment; the update part of the header must be a variable assignment or increment.

Throwing Exceptions

An exception can be only thrown by a statement of form throw new Exception(string) where string denotes a string literal, respectively a value of type java.lang.String.

Null

The keyword null may only appear on the right hand side of an initialization or assignment statement or on the right hand side of an equality or inequality expression.

Array Types

Currently only one-dimensional arrays are supported (i.e. the base type of an array must not itself be an array type).

References

The type system restricts a program such that that every object variable can be considered to hold the object value (rather than a reference to the value) which considerably simplifies reasoning about objects. This restriction ensures that two different references cannot denote the same object (and so an update of the object value via one reference cannot affect the object value denoted by any other reference). In particular,

• a variable of an object type may only receive the result of a constructor call or of a method call;
• a return statement may only return (the result of) a constructor call, a method call, or an object path v…, where v denotes a local variable of the current method;
• a method/constructor call may receive as an argument of an object type only (the result of) a constructor call, a method call, or an object path v… where v denotes a local variable or a method parameter that is not the base of an object path which appears as another argument in the same method/constructor call.

In the description above, an object path v… denotes the variable v, possibly trailed by a sequence of selectors of the form .var (an object variable selector) or [exp] (an array index selector).

Parameters

In a method, a parameter that denotes an object or array must not be assigned a new value (but the contents of the object or array may be modified). The reason is that the RISC ProgramExplorer handles such parameters as “transient” (the corresponding arguments may have new values after the call of the method); the restriction ensures that this view coincides with the Java semantics of object/array parameters holding pointers.

Java Classes The RISC ProgramExplorer does not itself provide/implement the classes of the Java API (also not the classes java.lang.String used for character strings or the class java.lang.System used for standard input/output); if such classes are used in programs, the programmer must provide corresponding class stubs in (a subpackage of) a package java within the . If no class String is provided, strings are represented by a built-in STRING type.

Specification Comments The contents of program comments of the form /*@ …@*/ and //@ … are interpreted as formal program specifications; the language of these specifications are explained in the following section.