The logic language of the RISC ProgramExplorer is based on the language of the RISC ProofNavigator [5, 8]. In the following, we only describe the differences respectively extensions.
The logic language allows to introduce by declarations
While the language of RISC ProofNavigator considers both terms and formulas as elements of the syntactic domain (value) expression (formulas are just expressions denoting a Boolean value, mismatches between terms and formulas are detected by the type checker), the RISC ProgramExplorer decomposes expression into two syntactic domains term and formula (which already enables the parser to detect mismatches). Nevertheless, on the semantic level predicates are just considered as functions whose result is a Boolean value.
Object/function/predicate constants can now be defined as follows:
The RISC ProgramExplorer introduces the additional types
STRING is an unspecified type which plays a role in the .
PREDICATE(types) is a synonym of
The use of this type syntactically simplifies the .
Type LOGICAL with constants LOGICALTRUE and LOGICALFALSE is the result type of predicates, respectively the type of those expressions that denote logical formulas (the predicate constants LOGICALTRUE and LOGICALFALSE thus denote formulas).
Type BIT with the constants BITTRUE and BITFALSE and associated operations &, | and ̃ is the type of truth values (the constants BITTRUE and BITFALSE thus denote terms).
Depending on the property settings (see Section 2), type code BOOLEAN is a synom for one of these types (and the constants TRUE and FALSE are synonyms for the corresponding constants). The difference only matters, if the selected logic is first order, because then formulas (denoting logical values) and terms (denoting other kinds of values) are strictly separated.
The subsequent subsections describe how a logical formula may refer to the values of . This requires the mapping of program values to logical values and of program types to logical types. The mapping is based on the automatically generated theory Base in the unnamed top-level package:
In detail, program types are mapped to logical types as follows (where we assume that the logical type BOOLEAN is a synonym for the logical type BIT of truth values):
The theory also contains an array type Array to which the program type (class) C[] is mapped (see below for the details of array representations).
Additionally the automatically generated theory contains the following constants:
In the translation of an object access object.field, the RISC ProgramExplorer uses the precondition object.null = FALSE. If an object, for which this precondition can be established is updated by an assignment to an object variable, also the new object value satisfies that condition. On the other side, null is just an unspecified value for which the precondition simply can not be established. As a consequence, in method preconditions not the test object /=C.null but the test NOTobject.null must be applied. Therefore also a program test object != null is automatically translated to the logical test object.null = FALSE.
However, if the user does not provide such a class, string literals in programs are considered as values of a pseudo-type that is mapped to the logical type .
The record type contains the following fields:
A class T contains also constants nullTArray and newTArray that represent array values that are null respectively result from the allocation of a new array (see above).
If T is boolean, int, char, or String, the theory Base contains also constants nullTArray and newTArray (again the name of T is capitalized) that represent array values that are null respectively result from the allocation of a new array.
As for objects, in method preconditions not the test array /=T.null but the test array.null = FALSE must be applied (see the explanation for objects above).
Description Within the context of a state predicate of a specification (e.g. in a or in a ), both OLD var and VAR var refer to the “current” state of the program variable var.
Within the context of a state relation of a specification (e.g. a or ), OLD var refers to the value of the program variable var in the prestate of the specified execution; VAR var refers to the value of var in the corresponding poststate.
More specifically, OLD var respectively VAR var denotes the logical value to which the value of the program variable is mapped. Therefore the type of OLD var respectively VAR var is the logical type to which the type of the program variable is mapped.
Pragmatics A reference to a program variable var in a formula is tagged with keyword OLD or VAR to explicitly distinguish it from a reference to a logical variable; we thus emphasize that its value actually results from mapping a program value to a logical value.
We choose the keywords and their interpretations in both state conditions and state relations in order to minimize the confusion of programmers:
However, if there is no corresponding state relation, the syntax OLD var in a state condition looks awkward since the condition only refers to a single state: here we may prefer VAR var.
The logic language introduces a new kind of values called states with corresponding types, constants, functions, and predicates.
Description A type of this family denotes the set of states that may result from the execution of a command. The type STATE indicates that the execution of the command must not return a value (i.e. that the command is executed within a function of result type void); the type STATE(type) indicates that the command may return a value of the denoted type.
Description Within the context of a state predicate of a specification (e.g. a ), both constants NOW and NEXT denote the “current” state.
Within the context of a state relation of a specification (e.g. a or ), the constant NOW denotes the prestate of the specified execution while the constant NEXT denotes the corresponding poststate.
Pragmatics To simplify the semantics, NEXT is also defined in the context of a state predicate.
In a loop invariant, NOW refers to the prestate of the loop, while NEXT refers to the poststate of the loop body.
Description These functions are evaluated over state whose type is of form . If state results from the execution of return value, then the term VALUE@next refers to (the logical mapping of) value. The type of state must be of form STATE(result); the type of VALUE@next is result (which is the logical mapping of the type of value).
If state results from the execution of throw new exception(message), the term MESSAGE@next refers to (the logical mapping of) message. Its type is the logical mapping of the program type java.lang.String (which must be the type of message).
Description These predicates are evaluated over state whose type is of form :
Description This predicate is evaluated over two states state1 and state2 which may be of different state types STATE(type1) and STATE(type2) (respectively STATE). The result is true if and only if both states are equal except for their values VALUE@state1 respectively VALUE@state2 (if applicable).
Pragmatics The predicate may be required to express the relationship between the poststate of a called method and the poststate of the calling method (which may have different return types).
Description These formulas are evaluated in the context of a pair of execution states (e.g. a or ) called the “prestate” and the “poststate” of the execution.
READSONLY is true if and only if the value of every program variable is in the poststate of the execution the same as in the prestate.
WRITESONLY name, … is true if and only if the value of every program variable that is not listed in “var, …” is in the poststate of the execution the same as in the prestate.