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    }