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 }