org.jmlspecs.jml4.rac
Class RacOldExpression

java.lang.Object
  org.jmlspecs.jml4.rac.PreValueManager.Entry
      org.jmlspecs.jml4.rac.RacOldExpression

public class RacOldExpression
extends PreValueManager.Entry

A RAC representation of a JML old expression. A JML old expression is translated into a new field of which value is set in the precondition check method by evaluating the expression; postcondition methods refer to the field to get the value of the old expression. For example, given an old expression \old(x + 1), the translation produces:

   ((java.lang.Integer) rac$old0.value()).intValue()
  

where rac$old0 is a new field introduced to store the value of the old expression. The field is declared as follows.

   private [static] JMLRacValue rac$old0;
  

And its value is assigned in the precondition check method as follows.

   rac$old0 = JMLRacValue.ofObject(new java.lang.Integer(x + 1));
  

This class represents an old expression as a pair of a field name and a (translated) expression.

Author:

Yoonsik Cheon and Amritam Sarcar

Constructor Summary

RacOldExpression(java.lang.String name, java.lang.String expr, boolean isStatic)
Creates a new instance with default spec var as false.

RacOldExpression(java.lang.String name, java.lang.String expr, boolean isStatic, boolean isSpecVar)
Creates a new instance with spec var as true.

RacOldExpression(java.lang.String name, java.lang.String expr, boolean isStatic, java.lang.String defaultValue)
Creates a new instance of JmlCacheExpression type.

Method Summary

java.lang.String	expression() Returns the translated expression.
boolean	isSpecVar() Returns whether the old expression is a specification variable declaration.

Methods inherited from class org.jmlspecs.jml4.rac.PreValueManager.Entry

isStatic, name, toString, type

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

RacOldExpression

public RacOldExpression(java.lang.String name,
                        java.lang.String expr,
                        boolean isStatic)

Creates a new instance with default spec var as false.

RacOldExpression

public RacOldExpression(java.lang.String name,
                        java.lang.String expr,
                        boolean isStatic,
                        boolean isSpecVar)

Creates a new instance with spec var as true.

RacOldExpression

public RacOldExpression(java.lang.String name,
                        java.lang.String expr,
                        boolean isStatic,
                        java.lang.String defaultValue)

Creates a new instance of JmlCacheExpression type.

Method Detail

expression

public java.lang.String expression()

Returns the translated expression. The return string has the following form:

  JMLRacValue.ofObject(new java.lang.Integer([[E]]);
 

where [[E]] is a translation of the original expression.

isSpecVar

public boolean isSpecVar()

Returns whether the old expression is a specification variable declaration.