    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.prover;
    004
    005    /**
    006     * An object of this class represent a "result" produced by Simplify.
    007     *
    008     * @see Simplify
    009     * @see escjava.prover.CECEnum
    010     * @see SExp
    011     */
    012
    013    public class SimplifyResult extends SimplifyOutput
    014    {
    015        /*@ spec_public @*/ SList labels;
    016        /*@ spec_public @*/ SList context;
    017
    018        //@ ensures \result == labels;
    019        public /*@ pure @*/ SList getLabels() {
    020            return labels;
    021        }
    022
    023        //@ ensures \result == context;
    024        public /*@ pure @*/ SList getContext() {
    025            return context;
    026        }
    027
    028        //@ requires COUNTEREXAMPLE <= kind && kind < END;
    029        //@ ensures this.kind == kind;
    030        //@ ensures this.labels == labels;
    031        //@ ensures this.context == context;
    032        SimplifyResult(int kind, SList labels, SList context) {
    033            super(kind);
    034            this.labels = labels;
    035            this.context = context;
    036        }
    037
    038        public /*@ pure non_null @*/ String toString() {
    039            return super.toString() + " labels=" + labels + " context=" + context;
    040        }
    041    }