001    package escjava.prover;
002    
003    public class SammyResponse extends ProverResponse {
004    
005        // placeholder for factory for building ProverResponses
006        /*@ 
007          @ ensures return_code == 1 ==> \result == ProverResponse.OK;
008          @ ensures return_code == -1 ==> \result == ProverResponse.FAIL;
009          @ ensures return_code == -2 ==> \result == ProverResponse.SYNTAX_ERROR;
010          @
011          @*/
012        static public /*@ pure non_null @*/ ProverResponse factory(int return_code) {
013            switch(return_code){
014              
015            case 1 :
016                return ProverResponse.OK;
017            case -1 :
018                return ProverResponse.FAIL;
019            case -2 :
020                return ProverResponse.SYNTAX_ERROR;
021            default : //positive attitude
022                return ProverResponse.OK;
023            }
024        }
025    
026    }