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 }