UTJML

edu.utep.cs.utjml.compiler.rt
Class JMLTestCoverage

java.lang.Object
  extended by edu.utep.cs.utjml.compiler.rt.JMLTestCoverage

public class JMLTestCoverage
extends Object

An experimental class to record condition coverage information of a postcondition. The runtime assertion checking code---in particular, the postcondition checking code---is assumed to call the exported methods to record the covered (called) atomic boolean expressions with their values. The atomic boolean expressions of a postcondition is identified with unique integer identification numbers, such as 1, 2, etc.

Version:
$Revision: 1.2 $
Author:
Yoonsik Cheon

Nested Class Summary
static class JMLTestCoverage.CInfo
          Class representing coverage of an atomic boolean expression.
 
Constructor Summary
JMLTestCoverage()
           
 
Method Summary
static void clear()
          Removes all the log entries.
static void init()
          Initialze internal data structures.
static int[] intLog()
          Returns an array consisting of the identifiers of the log entries accumulated so far.
static JMLTestCoverage.CInfo[] log()
          Returns an array of log entries accumulated so far.
static void log(int exprId)
          Records the the given atomic boolean expression, exprId, was evaluated to an undefined value.
static void log(int exprId, boolean val)
          Records that the given atomic boolean expression, exprId, was evaluated to the given value, val.
static int numOfExprs()
          Returns the number of atomic boolean expressions.
static void numOfExprs(int num)
          Sets the number of atomic boolean expressions.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

JMLTestCoverage

public JMLTestCoverage()
Method Detail

init

public static void init()
Initialze internal data structures. This method should be called prior to a postcondition evaluation by the assertion checking code.


numOfExprs

public static void numOfExprs(int num)
Sets the number of atomic boolean expressions. This method should be called by the assertion checking code.


numOfExprs

public static int numOfExprs()
Returns the number of atomic boolean expressions.


log

public static void log(int exprId,
                       boolean val)
Records that the given atomic boolean expression, exprId, was evaluated to the given value, val. This method should be called by the assertion checking code.


log

public static void log(int exprId)
Records the the given atomic boolean expression, exprId, was evaluated to an undefined value. An undefined value can be angelic (e.g., non-executable) or demonic (e.g., exception). This method should be called by the assertion checking code.


log

public static JMLTestCoverage.CInfo[] log()
Returns an array of log entries accumulated so far. An empty array is returned if there is no log accumulated.


intLog

public static int[] intLog()
Returns an array consisting of the identifiers of the log entries accumulated so far. An empty array is returned if there is no log.


clear

public static void clear()
Removes all the log entries.


UTJML

UTJML is Copyright (C) 2004-2006 by University of Texas at El Paso and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the JML project.