    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    }