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

java.lang.Object
  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.