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 }