    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    }