001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package escjava.prover;
004    
005    /**
006     * Objects of this class represent the summary part of the normal output
007     * from Simplify: valid, invalid, or unknown.
008     * 
009     * @see Simplify
010     * @see escjava.prover.CECEnum
011     * @see SExp
012     */
013    
014    public class SimplifyOutputSentinel extends SimplifyOutput
015    {
016        /*@ spec_public @*/ int number;
017    
018        /*@ normal_behavior
019          @   requires kind == VALID || kind == INVALID || kind == UNKNOWN;
020          @   modifies this.number;
021          @   ensures this.kind == kind;
022          @   ensures this.number == number;
023          @*/
024        SimplifyOutputSentinel(int kind, int number) {
025            super(kind);
026            this.number = number;
027        }
028                                                    
029        public /*@ pure non_null @*/ String toString() {
030            return super.toString() + " number=" + number;
031        }
032    }