Discrepancy.java

package edu.udel.cis.vsl.tass.predicate.impl;

import edu.udel.cis.vsl.tass.dynamic.IF.DynamicException;
import edu.udel.cis.vsl.tass.dynamic.IF.DynamicFactoryIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ReferenceValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ValueIF;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionProblem.Certainty;
import edu.udel.cis.vsl.tass.util.TernaryResult.ResultType;

/**
 * A discrepancy pinpoints an expected value and actual value that disagree. If
 * it is the case that the expectValue cannot be proved equal to the
 * actualValue, we say the Discrepancy object is "discrepant".
 * 
 * Immutable pattern: fields cannot be modified after instantation. Exception:
 * derived values.
 */
public class Discrepancy {

	private DynamicFactoryIF dynamicFactory;

	private ValueIF assumption;

	private ReferenceValueIF expectedReference;

	private ValueIF expectedValue;

	private ReferenceValueIF actualReference;

	private ValueIF actualValue;

	/**
	 * If discrepancyCached is true, a null certainty means this is not
	 * discrepant. Otherwise, this field is not used. A non-null certainty means
	 * this is discrepant, and the certainty gives the level of certainty of the
	 * disagreement between actual and expected values.
	 */
	private Certainty certainty;

	/** Have we already computed whether this is discrepant? */
	private boolean discrepancyCached;

	/**
	 * If you already know whether this is discrepant and have computed the
	 * certainty, use this constructor.
	 */
	public Discrepancy(DynamicFactoryIF dynamicFactory, ValueIF assumption,
			ReferenceValueIF expectedReference, ValueIF expectedValue,
			ReferenceValueIF actualReference, ValueIF actualValue,
			Certainty certainty) {
		this.dynamicFactory = dynamicFactory;
		this.assumption = assumption;
		this.expectedReference = expectedReference;
		this.expectedValue = expectedValue;
		this.actualReference = actualReference;
		this.actualValue = actualValue;
		this.certainty = certainty;
		discrepancyCached = true;
	}

	/** Constructs new object in which discrepancy has not yet been computed. */
	public Discrepancy(DynamicFactoryIF dynamicFactory, ValueIF assumption,
			ReferenceValueIF expectedReference, ValueIF expectedValue,
			ReferenceValueIF actualReference, ValueIF actualValue) {
		this.dynamicFactory = dynamicFactory;
		this.assumption = assumption;
		this.expectedReference = expectedReference;
		this.expectedValue = expectedValue;
		this.actualReference = actualReference;
		this.actualValue = actualValue;
		this.certainty = null;
		discrepancyCached = false;
	}

	public ReferenceValueIF expectedReference() {
		return expectedReference;
	}

	public ValueIF expectedValue() {
		return expectedValue;
	}

	public ReferenceValueIF actualReference() {
		return actualReference;
	}

	public ValueIF actualValue() {
		return actualValue;
	}

	public Certainty certainty() {
		return certainty;
	}

	public ValueIF assumption() {
		return assumption;
	}

	public boolean isDiscrepant() throws DynamicException {
		if (!discrepancyCached) {
			ValueIF assertion = dynamicFactory.equals(assumption,
					expectedValue, actualValue);
			ResultType truth = dynamicFactory.valid(assumption, assertion);

			if (truth == ResultType.YES) {
				certainty = null;
			} else {
				if (truth == ResultType.MAYBE) {
					certainty = Certainty.MAYBE;
				} else {
					certainty = Certainty.PROVEABLE;
				}
			}
			discrepancyCached = true;
		}
		return certainty != null;
	}

	private String dereference(ReferenceValueIF reference) {
		String address = reference.toString();

		if (address.startsWith("&")) {
			return address.substring(1);
		} else {
			return "*(" + address + ")";
		}
	}

	public String explanation() {
		if (certainty == null) {
			return null;
		} else {
			String explanation;

			if (certainty == Certainty.MAYBE) {
				explanation = "Cannot prove that final values of implementation and specification agree:";
			} else {
				explanation = "It is possible for the final values of implementation and specification to disagree:";
			}
			explanation += "\n\nSpecification  output "
					+ dereference(expectedReference) + ":\n  " + expectedValue;
			explanation += "\n\nImplementation output "
					+ dereference(actualReference) + ":\n  " + actualValue + "\n";

			return explanation;
		}
	}
}