public class Verif2015 {
		
		/*@
			@ requires s != null;
			@ ensures (\result <==> (\forall integer i; 
			@ (0 <= i < s.length) ==>
			@ (s[i] == s[(s.length  -i -1 )])));
		*/
		public static boolean palindrome (boolean[] s){
		
						int low = 0;
						int high = s.length -1 ;
						/*@ loop_invariant  0 <= low && high < s.length && 
							@ high + low == s.length -1 &&
							@ (\forall integer k; (0 <= k < low ==>
							@ s[k] == s[(s.length -k -1 )]));
							@ loop_variant  high - low;
							@*/

						while (low < high && s[low] == s[high]) {
								low ++;
								high --;
						}
				
						return low >= high;
		}
		
}